text:
/-
Copyright (c) 2022. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Moritz Firsching, Fabian Kruse, Nikolas Kuhn.
-/
import tactic
import analysis.special_functions.log
import analysis.special_functions.pow
import algebra.big_operators.basic
import algebra.big_operators.intervals
import data.finset.sum
import data.fintype.basic
import data.real.basic
import data.real.pi.wallis
import order.filter
import order.filter.basic
import order.bounded_order
import topology.instances.real
import topology.instances.ennreal

/-!
# Stirling's formula

This file proves Theorem 90 from the [100 Theorem List] <https://www.cs.ru.nl/~freek/100/>.
It states that $n!$ grows asymptotically like $\sqrt{2\pi n}(\frac{n}{e})^n$.

## Proof outline

The proof follows: <https://proofwiki.org/wiki/Stirling%27s_Formula>.

We proceed in two parts.
### Part 1
We consider the fraction sequence $a_n$ of fractions $n!$ over $\sqrt{2n}(\frac{n}{e})^n$ and
proves that this sequence converges against a real, positve number $a$. For this the two main
ingredients are
 - taking the logarithm of the sequence and
 - use the series expansion of $\log(1 + x)$.

### Part 2
We use the fact that the series defined in part 1 converges againt a real number $a$ and prove that
$a = \sqrt{\pi}$. Here the main ingredient is the convergence of the Wallis product.
-/

namespace stirling

open_locale big_operators -- notation ∑ for finite sums
open_locale classical real topological_space nnreal ennreal filter big_operators
open real
open finset
open nat
open filter

/-- TODO: Perhaps something to add as rat.cast_sum in more generality (see below) in mathlib?!-/
lemma rat_cast_sum (s : finset ℕ) (f : ℕ → ℚ) :
  ↑(∑ n in s, f n : ℚ) = (∑ n in s, (f n : ℝ)) :=
  (rat.cast_hom ℝ).map_sum f s
-- @[simp, norm_cast] lemma rat_cast_sum [add_comm_monoid β] [has_one β]
-- (s : finset α) (f : α → ℚ) :
-- ↑(∑ x in s, f x : ℚ) = (∑ x in s, (f x : β)) := by sorry

/-- **Sum of the Reciprocals of the Triangular Numbers**
 (copied from archive)
 TODO: include in some form mathlib or figure out how to import it from archive/ --/
lemma inverse_triangle_sum :
  ∀ n, ∑ k in range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n :=
begin
  refine sum_range_induction _ _ (if_pos rfl) _,
  rintro (_|n), { rw [if_neg, if_pos]; norm_num },
  simp_rw [if_neg (succ_ne_zero _), succ_eq_add_one],
  have A : (n + 1 + 1 : ℚ) ≠ 0, by { norm_cast, norm_num },
  push_cast,
  field_simp [cast_add_one_ne_zero],
  ring,
end

/-- **Sum of products of consecutive reciprocals** -/
lemma partial_sum_consecutive_reciprocals :
 ∀ n, ∑ k in range n, (1 : ℚ) / (k.succ * (k.succ.succ)) ≤ 1 :=
begin
  intro n,
  rw [← (mul_le_mul_left (zero_lt_two)), mul_sum], swap, { exact rat.nontrivial },
  { have h : ∀ (k : ℕ), k ∈ (range n) →
      2 * ((1 : ℚ) / (k.succ * (k.succ.succ))) = 2 / (k.succ * (k.succ.succ)),
      by { intros k hk, rw [mul_div], rw [mul_one (2 : ℚ)] },
    rw sum_congr rfl h,
    have h₁ := inverse_triangle_sum n.succ,
    rw sum_range_succ' at h₁,
    norm_num at *,
    rw h₁,
    rw [sub_le_self_iff],
    refine (le_div_iff _).mpr (_),
    { exact (cast_lt.mpr n.succ_pos), },
    { rw [zero_mul], exact zero_le_two, } },
 end

/-!
 ### Part 1
 https://proofwiki.org/wiki/Stirling%27s_Formula#Part_1
-/

/--
A sequence of real numbers `an n` has limit `a`, if and only if only if the shifted
sequence given by `an n.succ` has the limit `a`.
-/
lemma tendsto_succ (an : ℕ → ℝ) (a : ℝ) : tendsto an at_top (𝓝 a) ↔
  tendsto (λ n : ℕ, (an n.succ)) at_top (𝓝 a) :=
begin
  nth_rewrite_rhs 0 ← tendsto_map'_iff,
  have h : map succ at_top = at_top :=
  begin
    rw map_at_top_eq_of_gc pred 1,
    { exact @succ_le_succ, },
    { intros a b hb,
      cases (exists_eq_succ_of_ne_zero (one_le_iff_ne_zero.mp hb)) with d hd,
      rw [hd, pred_succ],
      exact succ_le_succ_iff, },
    { intros b hb,
      cases (exists_eq_succ_of_ne_zero (one_le_iff_ne_zero.mp hb)) with d hd,
      rw hd,
      rw pred_succ, },
  end,
  rw h,
end

/--
Define `an n` as $\frac{n!}{\sqrt{2n}/(\frac{n}{e})^n$.
Stirling's formula states that this sequence has limit $\sqrt(π)$.
-/
noncomputable def an (n : ℕ) : ℝ := (n.factorial : ℝ) / ((sqrt(2 * n) * ((n / (exp 1))) ^ n))

/-- The function `log(1 + x) - log(1 - x)` has a power series expansion with k-th term
`2 * x^(2 * k + 1) / (2 * k + 1)`, valid for `|x| < 1`. -/
lemma log_sum_plus_minus (x : ℝ) (hx : |x| < 1) : has_sum (λ k : ℕ,
  (2 : ℝ) * (1 / (2 * (k : ℝ) + 1)) * (x ^ (2 * k + 1))) (log (1 + x) - log(1 - x)) :=
begin
 have h₁, from has_sum_pow_div_log_of_abs_lt_1 hx,
  have h₂, from has_sum_pow_div_log_of_abs_lt_1 (eq.trans_lt (abs_neg x) hx),
  replace h₂ := (has_sum_mul_left_iff  (λ h:(-1 = (0:ℝ)), one_ne_zero (neg_eq_zero.mp h))).mp h₂,
  rw [neg_one_mul, neg_neg, sub_neg_eq_add 1 x] at h₂,
  have h₃, from has_sum.add h₂ h₁,
  rw [tactic.ring.add_neg_eq_sub] at h₃,
  let term := (λ n :ℕ, ((-1) * ((-x) ^ (n + 1) / ((n : ℝ) + 1)) + (x ^ (n + 1) / ((n : ℝ) + 1)))),
  let two_mul := (λ (n : ℕ), (2 * n)),
  rw ←function.injective.has_sum_iff (mul_right_injective two_pos) _ at h₃,
  { suffices h_term_eq_goal :
    (term ∘ two_mul) = (λ k : ℕ, 2 * (1 / (2 * (k : ℝ) + 1)) * x ^ (2 * k  + 1)),
    by {rw h_term_eq_goal at h₃, exact h₃},
    apply funext,
    intro n,
    rw [function.comp_app],
    dsimp only [two_mul, term],
    rw odd.neg_pow (⟨n, rfl⟩ : odd (2 * n + 1)) x,
    rw [neg_one_mul, neg_div, neg_neg, cast_mul, cast_two],
    ring },
  { intros m hm,
    rw [range_two_mul, set.mem_set_of_eq] at hm,
    rw [even.neg_pow (even_succ.mpr hm), succ_eq_add_one, neg_one_mul, neg_add_self] },
end

/--
For any natural number `n ≠ 0`, we have the identity
`log((n + 1) / n) = log(1 + 1 / (2*n + 1)) - log(1 - 1/(2*n + 1))`.
-/
lemma aux_log (n : ℕ) (hn : n ≠ 0) :
  log (n.succ / n) = log (1 + 1 / (2 * n + 1)) - log (1 - 1 / (2 * n + 1)) :=
begin
  have : (2 : ℝ) * n + 1 ≠ 0, by { norm_cast, exact (2 * n).succ_ne_zero, },
  rw ← log_div,
  suffices h, from congr_arg log h,
    all_goals {field_simp [cast_ne_zero.mpr]}, /- all_goals prevents using brackets here -/
  { ring },
  { norm_cast, exact succ_ne_zero (2 * n + 1) },
end

/--
For any natural number `n`, the expression `log((n + 1) / n)` has the series expansion
$\sum_{k=0}^{\infty}\frac{2}{2k+1}(\frac{1}{2n+1})^{2k+1}$.
-/
lemma power_series_ln (n : ℕ) (hn : n ≠ 0) : has_sum (λ (k : ℕ),
  (2 : ℝ) * (1 / (2 * (k : ℝ) + 1)) * ((1 / (2 * (n : ℝ) + 1)) ^ (2 * k + 1)))
  (log ((n.succ : ℝ) / (n : ℝ))) :=
 begin
  have h₀ : (0 < n), from zero_lt_iff.mpr hn,
  have h₁ : |1 / (2 * (n : ℝ) + 1)| < 1, by --in library??
  { rw [abs_of_pos, div_lt_one]; norm_cast,
    any_goals {linarith}, /- can not use brackets for single goal, bc of any_goals -/
    { exact div_pos one_pos (cast_pos.mpr (2 * n).succ_pos) }, },
  rw aux_log n (hn),
  exact log_sum_plus_minus (1 / (2 * (n : ℝ) + 1)) h₁,
 end

/--
`bn n` is log of `an n`.
-/
noncomputable def bn (n : ℕ) : ℝ := log (an n)

/--
For each natural number `n ≠ 0`, we have $0<\sqrt{2n}$.
-/
lemma zero_lt_sqrt_two_n (n : ℕ) (hn : n ≠ 0) : 0 < sqrt (2 * (n : ℝ)) :=
   real.sqrt_pos.mpr (mul_pos two_pos (cast_pos.mpr (zero_lt_iff.mpr hn)))

/--
We have the expression `bn (n+1) = log(n + 1)! - 1 / 2 * log(2 * n) - n * log ((n + 1) / e)`.
-/
lemma bn_formula (n : ℕ): bn n.succ = (log (n.succ.factorial : ℝ)) -
  1 / (2 : ℝ) * (log (2 * (n.succ : ℝ))) - (n.succ : ℝ) * log ((n.succ : ℝ) / (exp 1)) :=
begin
  have h3, from (lt_iff_le_and_ne.mp (zero_lt_sqrt_two_n n.succ (succ_ne_zero n))).right,
  have h4 : 0 ≠ ((n.succ : ℝ) / exp 1) ^ n.succ, from
    ne_of_lt ((pow_pos (div_pos (cast_pos.mpr n.succ_pos ) (exp_pos 1)) (n.succ))),
  rw [bn, an, log_div, log_mul, sqrt_eq_rpow, log_rpow, log_pow],
  { linarith },
  { exact (zero_lt_mul_left zero_lt_two).mpr (cast_lt.mpr n.succ_pos),},
  { exact h3.symm, },
  { exact h4.symm, },
  { exact cast_ne_zero.mpr n.succ.factorial_ne_zero, },
  { apply (mul_ne_zero h3.symm h4.symm), },
end

/--
The sequence `bn (m + 1) - bn (m + 2)` has the series expansion
   `∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))`
-/
lemma bn_diff_has_sum (m : ℕ) :
  has_sum (λ (k : ℕ), (1 : ℝ) / (2 * k.succ + 1) * ((1 / (2 * m.succ + 1)) ^ 2) ^ (k.succ))
  ((bn m.succ) - (bn m.succ.succ)) :=
begin
  have hx : ∀ (n : ℕ), (bn n.succ) - (bn n.succ.succ) =
    ((n.succ : ℝ) + 1 / (2 : ℝ)) * log(((n.succ.succ) : ℝ) / (n.succ : ℝ)) - 1 :=
  begin
    intro n,
    have h_reorder : ∀ {a b c d e f : ℝ}, a - 1 / (2 : ℝ) * b - c - (d - 1 / (2 : ℝ) * e - f) =
      (a - d) - 1 / (2 : ℝ) * (b - e) - (c - f),
    by {intros, ring_nf},
    rw [bn_formula, bn_formula, h_reorder],
    repeat {rw [log_div, factorial_succ]},
    push_cast,
    repeat {rw log_mul},
    rw log_exp,
    ring_nf,
    all_goals {norm_cast},
    all_goals {try {refine mul_ne_zero _ _}, try {exact succ_ne_zero _}},
    any_goals {exact factorial_ne_zero n},
    any_goals {exact exp_ne_zero 1},
  end,
  have h_sum₀, from power_series_ln m.succ (succ_ne_zero m),
  have h_nonzero : (m.succ : ℝ) + 1 / (2 : ℝ) ≠ 0,
  by {rw cast_succ, field_simp, norm_cast, linarith}, --there has to be a better way...
  rw has_sum_mul_left_iff h_nonzero at h_sum₀,
  have h_inner : ∀ (b : ℕ) , (((m.succ : ℝ) + 1 / 2) * (2 * (1 / (2 * (b : ℝ) + 1)) *
      (1 / (2 * (m.succ : ℝ) + 1)) ^ (2 * b + 1)))
      = (1 : ℝ) / (2 * (b : ℝ) + 1) * ((1 / (2 * m.succ + 1)) ^ 2) ^ b :=
  begin
    intro b,
    rw [← pow_mul, pow_add],
    have : 2 * (b : ℝ) + 1     ≠ 0, by {norm_cast, exact succ_ne_zero (2*b)},
    have : 2 * (m.succ :ℝ) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2*m.succ)},
    field_simp,
    rw mul_comm _ (2 : ℝ),
    exact mul_rotate' _ _ _,
  end,
  have h_sum₁ : has_sum (λ (b : ℕ),
    ((1 : ℝ) / (2 * (b : ℝ) + 1) * ((1 / (2 * m.succ + 1)) ^ 2) ^ b))
    (((m.succ : ℝ) + 1 / 2) * log ((m.succ.succ : ℝ) / (m.succ : ℝ))) :=
  begin
    refine has_sum.has_sum_of_sum_eq _ h_sum₀,
    intros,
    use u,
    intros,
    use v',
    split,
    { exact ᾰ },
    { refine sum_congr rfl _, intros k hk, exact h_inner k },
  end,
  have h_sum : tendsto
    (λ (n : ℕ), ∑ (k : ℕ) in range n.succ,
    (λ (b : ℕ), 1 / (2 * (b : ℝ) + 1) * ((1 / (2 * (m.succ : ℝ) + 1)) ^ 2) ^ b) k)
    at_top (𝓝 (((m.succ : ℝ) + 1 / 2) * log ((m.succ.succ : ℝ) / (m.succ : ℝ)))) :=
    (has_sum.tendsto_sum_nat h_sum₁).comp (tendsto_add_at_top_nat 1),
  have split_zero : ∀ (n : ℕ), ∑ (k : ℕ) in range n.succ,
    1 / (2 * (k : ℝ) + 1) * ((1 / (2 * (m.succ : ℝ) + 1)) ^ 2) ^ k =
    (∑ (k : ℕ) in range n,
    1 / (2 * (k.succ : ℝ) + 1) * ((1 / (2 * (m.succ : ℝ) + 1)) ^ 2) ^ k.succ) + 1 := by
    { intro n,
      rw sum_range_succ' (λ (k : ℕ),
        1 / (2 * (k : ℝ) + 1) * ((1 / (2 * (m.succ : ℝ) + 1)) ^ 2) ^ k) n,
      dsimp only [], --beta reduce functions
      rw [pow_zero, mul_one, cast_zero, mul_zero, zero_add, div_one] },
  replace h_sum := tendsto.congr split_zero h_sum,
  replace h_sum := tendsto.add_const (-1) h_sum,
  simp only [add_neg_cancel_right] at h_sum, --beta reduce and rw?
  rw tactic.ring.add_neg_eq_sub _ (1 : ℝ) at h_sum,
  rw ← hx at h_sum,
  exact (summable.has_sum_iff_tendsto_nat
    ((summable_nat_add_iff 1).mpr (has_sum.summable h_sum₁))).mpr h_sum,
end

/-- The sequence `bn` is monotone decreasing -/
lemma bn_antitone : ∀ (n m : ℕ), n ≤ m → bn m.succ ≤ bn n.succ :=
begin
  apply antitone_nat_of_succ_le,
  intro n,
  refine sub_nonneg.mp _,
  rw ← succ_eq_add_one,
  refine has_sum.nonneg _ (bn_diff_has_sum n),
  norm_num,
  simp only [one_div],
  intro m,
  refine mul_nonneg _ _,
  all_goals {refine inv_nonneg.mpr _, norm_cast, exact (zero_le _)},
end

/--
We have the bound  `bn n - bn (n+1) ≤ 1/(2n+1)^2* 1/(1-(1/2n+1)^2)`.
-/
lemma bn_diff_le_geo_sum : ∀ (n : ℕ),
  bn n.succ - bn n.succ.succ ≤ (1 / (2 * n.succ + 1)) ^ 2 / (1 - (1 / (2 * n.succ + 1)) ^ 2) :=
begin
  intro n,
  have g : has_sum (λ (k : ℕ), ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ)
    ((1 / (2 * n.succ + 1)) ^ 2 / (1 - (1 / (2 * n.succ + 1)) ^ 2)) :=
  begin
    have h_pow_succ := λ (k : ℕ),
      symm (pow_succ ((1 / (2 * ((n : ℝ) + 1) + 1)) ^ 2) k),
    have h_nonneg : 0 ≤ ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2),
    by { rw [cast_succ, one_div, inv_pow₀, inv_nonneg], norm_cast, exact zero_le', },
    have hlt : ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) < 1, by
    { simp only [cast_succ, one_div, inv_pow₀],
      refine inv_lt_one _,
      norm_cast,
      simp only [nat.one_lt_pow_iff, ne.def, zero_eq_bit0, nat.one_ne_zero, not_false_iff,
        lt_add_iff_pos_left, canonically_ordered_comm_semiring.mul_pos, succ_pos', and_self], },
    have h_geom := has_sum_geometric_of_lt_1 h_nonneg hlt,
    have h_geom' := has_sum.mul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) h_geom,
    norm_num at h_geom',
    norm_num at h_pow_succ,
    have h_geom'' :
      has_sum (λ (b : ℕ), (1 / ((2 * ((n : ℝ) + 1) + 1) ^ 2) ^ b.succ))
      (1 / (2 * ((n : ℝ) + 1) + 1) ^ 2 * (1 - 1 / (2 * ((n : ℝ) + 1) + 1) ^ 2)⁻¹) :=
    begin
      refine has_sum.has_sum_of_sum_eq _ h_geom',
      intros,
      use u,
      intros,
      use v',
      split,
      { exact ᾰ },
      { refine sum_congr rfl _, intros k hk, exact h_pow_succ k },
    end,
    norm_num,
    exact h_geom'',
  end,
  have hab :
    ∀ (k : ℕ), (1 / (2 * (k.succ : ℝ) + 1)) * ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ ≤
    ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ :=
  begin
    intro k,
    have h_zero_le : 0 ≤ ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ, by
    { simp [cast_succ, one_div, inv_pow₀, inv_nonneg], norm_cast, exact zero_le', },
    have h_left : 1 / (2 * (k.succ : ℝ) + 1) ≤ 1, by
    { simp only [cast_succ, one_div],
      refine inv_le_one _,
      norm_cast,
      exact (le_add_iff_nonneg_left 1).mpr zero_le', },
    exact mul_le_of_le_one_left h_zero_le h_left,
  end,
  exact has_sum_le hab (bn_diff_has_sum n) g,
end

/--
We have the bound  `bn n - bn (n+1)` ≤ 1/(4n(n+1))
-/
lemma bn_sub_bn_succ : ∀ (n : ℕ),
bn n.succ - bn n.succ.succ ≤ 1 / (4 * n.succ * n.succ.succ) :=
begin
  intro n,
  have h₁ : 0 < 4 * (n.succ : ℝ) * (n.succ.succ : ℝ), by
  { norm_cast, simp only [canonically_ordered_comm_semiring.mul_pos, succ_pos', and_self], },
  have h₂ : 0 < 1 - (1 / (2 * (n.succ : ℝ) + 1)) ^ 2 :=
  begin
    refine sub_pos.mpr _,
    refine (sq_lt_one_iff _).mpr _,
    { rw one_div,
      refine inv_nonneg.mpr _,
      norm_cast,
      exact zero_le (2 * succ n + 1) },
    { refine (div_lt_one _).mpr _,
      all_goals {norm_cast},
      linarith,
      refine lt_add_of_pos_left 1 ((1 : ℕ).succ_mul_pos (succ_pos n)), },
  end,
  refine le_trans (bn_diff_le_geo_sum n) ((le_div_iff' h₁).mpr _),
  rw mul_div (4 * (n.succ : ℝ) * (n.succ.succ : ℝ))
    ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) (1 - (1 / (2 * (n.succ : ℝ) + 1)) ^ 2),
  refine (div_le_one h₂).mpr _,
  norm_num,
  rw mul_div,
  have h₃: 0 < (2 * ((n : ℝ) + 1) + 1) ^ 2 :=
  begin
    rw sq,
    norm_cast,
    simp only [canonically_ordered_comm_semiring.mul_pos,
    succ_pos', and_self],
  end,
  refine (div_le_iff' h₃).mpr _,
  rw mul_sub,
  norm_num,
  refine le_sub.mp _,
  rw mul_one_div,
  refine (div_le_iff' h₃).mpr ((le_mul_iff_one_le_right h₃).mpr
    (le_sub_iff_add_le.mpr _)),
  norm_cast,
  rw sq,
  linarith,
end

/-- For any `n`, we have `bn 1 - bn n ≤ 1/4` -/
lemma bn_bounded_aux : ∀ (n : ℕ), bn 1 - bn n.succ ≤ 1 / 4 :=
begin
  let bn' : (ℕ → ℝ) := λ (k : ℕ), bn k.succ,
  intro n,
  calc
  bn 1 - bn n.succ = bn' 0 - bn' n : rfl
   ... = ∑ k in range n, (bn' k - bn' (k + 1))          : by rw ← (sum_range_sub' bn' n)
   ... = ∑ k in range n, (bn k.succ - bn k.succ.succ)   : rfl
   ... ≤ ∑ k in range n, 1 / (4 * k.succ * k.succ.succ) : sum_le_sum (λ k, λ hk, bn_sub_bn_succ k)
   ... = ∑ k in range n, (1 / 4) * (1 / (k.succ * k.succ.succ)) :
   begin
     have hi : ∀ (k : ℕ), (1 : ℝ) / (4 * k.succ * k.succ.succ) =
      (1 / 4) * (1 / (k.succ * k.succ.succ)) :=
     begin
       intro k,
       norm_cast,
       field_simp,
       simp only [one_div, inv_inj],
       ring_nf,
     end,
    refine sum_congr rfl (λ k, λ hk, hi k),
   end
   ... = 1 / 4 * ∑ k in range n, 1 / (k.succ * k.succ.succ) : by rw mul_sum
   ... ≤ 1 / 4 * 1 :
   begin
     refine (mul_le_mul_left _).mpr _,
     { exact div_pos one_pos four_pos },
     { convert rat.cast_le.mpr (partial_sum_consecutive_reciprocals n),
       rw rat_cast_sum,
       push_cast,
       exact rat.cast_one.symm },
   end
   ... = 1 / 4 : by rw mul_one,
end

/-- The sequence `bn` is bounded below by `3/4 - 1/2 * log 2`  for `n ≥ 1`. -/
lemma bn_bounded_by_constant : ∀ (n : ℕ), 3 / (4 : ℝ) - 1 / 2 * log 2 ≤ bn n.succ :=
begin
  intro n,
  calc
  bn n.succ ≥ bn 1 - 1 / 4 : sub_le.mp (bn_bounded_aux n)
   ... = (log ((1 : ℕ).factorial) - 1 / 2 * log (2 * (1 : ℕ)) - (1 : ℕ) *
          log ((1 : ℕ) / (exp 1))) - 1 / 4 : by rw bn_formula 0
   ... = 0 - 1 / 2 * log 2 - log (1 / (exp 1)) - 1 / 4 :
      by simp only [factorial_one, cast_one, log_one, one_div, mul_one, log_inv, log_exp, mul_neg]
   ... = -1 / 2 * log 2 - log (1 / (exp 1)) - 1 / 4 : by ring
   ... = -1 / 2 * log 2 + 1 - 1 / 4  : by simp only [one_div, log_inv, log_exp, sub_neg_eq_add]
   ... = -1 / 2 * log 2 + 3 / 4      : by ring
   ... = 3 / (4 : ℝ) - 1 / 2 * log 2 : by ring,
end

/-- The sequence `bn` is bounded below. -/
lemma bn_has_lower_bound : (lower_bounds (set.range (λ (k : ℕ), bn k.succ))).nonempty :=
begin
   use 3 / (4 : ℝ) - 1 / 2 * log 2,
   intros,
   rw lower_bounds,
   rw [set.mem_set_of_eq],
   simp only [set.mem_range, forall_apply_eq_imp_iff', forall_exists_index],
   exact bn_bounded_by_constant,
end

/--
Any sequence `bn` of real numbers that is monotone decreasing and bounded below has
a limit in the real numbers.
-/
lemma monotone_convergence (bn : ℕ → ℝ) (h_sd : ∀ (n m : ℕ), n ≤ m → bn m ≤ bn n)
  (h_bounded : (lower_bounds (set.range bn)).nonempty) : ∃ (m : ℝ), tendsto bn at_top (𝓝 m) :=
begin
 use Inf (set.range bn),
 exact tendsto_at_top_is_glb h_sd (real.is_glb_Inf (set.range bn)
   (set.range_nonempty bn) h_bounded),
end

/-- The sequence `an` is positive for `n > 0`  -/
lemma an'_pos : ∀ (n : ℕ), 0 < an n.succ :=
 (λ n, div_pos (cast_pos.mpr (factorial_pos n.succ))
    (mul_pos ((real.sqrt_pos).mpr (mul_pos two_pos (cast_pos.mpr (succ_pos n))))
    (pow_pos (div_pos (cast_pos.mpr (succ_pos n)) (exp_pos 1)) n.succ)))

/--
The sequence `an` has the explicit lower bound exp (3/4 - 1/2 * log 2)
-/
lemma an'_bounded_by_pos_constant : ∀ (n : ℕ), exp (3 / (4 : ℝ) - 1 / 2 * log 2) ≤ an n.succ :=
begin
  intro n,
  rw ← (le_log_iff_exp_le (an'_pos n)),
  exact bn_bounded_by_constant n,
end

/-- The sequence `an` is monotone decreasing -/
lemma an'_antitone : ∀ (n m : ℕ), n ≤ m → an m.succ ≤ an n.succ :=
  (λ n, λ m, λ h, (log_le_log (an'_pos m) (an'_pos n)).mp (bn_antitone n m h))

/-- The sequence `an` has a lower bound -/
lemma an'_has_lower_bound : (lower_bounds (set.range (λ (k : ℕ), an k.succ))).nonempty :=
begin
   use exp (3 / (4 : ℝ) - 1 / 2 * log 2),
   intros,
   rw lower_bounds,
   simp only [set.mem_range, forall_exists_index, forall_apply_eq_imp_iff', set.mem_set_of_eq],
   exact an'_bounded_by_pos_constant,
end

/-- The sequence `an` converges to a real number -/
lemma an_has_limit_a : ∃ (a : ℝ), tendsto (λ (n : ℕ), an n) at_top (𝓝 a) :=
begin
  have ha := monotone_convergence (λ (k : ℕ), an k.succ) an'_antitone an'_has_lower_bound,
  cases ha with x hx,
  rw ← tendsto_succ an x at hx,
  use x,
  exact hx,
end

/-- The limit `a` of the sequence `an` satisfies `0 < a` -/
lemma an_has_pos_limit_a : ∃ (a : ℝ), 0 < a ∧ tendsto (λ (n : ℕ), an n) at_top (𝓝 a) :=
begin
  have h := an_has_limit_a,
  cases h with a ha,
  use a,
  split,
  { let an' : ℕ → ℝ := λ n, an n.succ,
    rw tendsto_succ an a at ha,
    have e_lower_bound : exp (3 / (4 : ℝ) - 1 / 2 * log 2) ∈ lower_bounds (set.range an') :=
    begin
      intros x hx,
      rw [set.mem_range] at hx,
      cases hx with k hk,
      rw ← hk,
      exact an'_bounded_by_pos_constant k,
    end,
    exact gt_of_ge_of_gt ((le_is_glb_iff (is_glb_of_tendsto_at_top an'_antitone ha)).mpr
      e_lower_bound) (3 / 4 - 1 / 2 * log 2).exp_pos },
  { exact ha },
end

/-!
 ### Part 2
 https://proofwiki.org/wiki/Stirling%27s_Formula#Part_2
-/

/--
Define `wallis_inside_prod n` as `2 * n / (2 * n - 1) * 2 * n/(2 * n + 1)`.
This is the term appearing inside the Wallis product
-/
noncomputable def wallis_inside_prod (n : ℕ) : ℝ :=
  (((2 : ℝ) * n) / (2 * n - 1)) * ((2 * n) / (2 * n + 1))

/--
We can shift the indexing in a product.
 -/
lemma aux1 (k : ℕ) : ∏ i in range k, (wallis_inside_prod (1 + i)) =
    ∏ i in Ico 1 k.succ, wallis_inside_prod i :=
begin
  rw [range_eq_Ico],
  rw prod_Ico_add wallis_inside_prod 0 k 1,
end

/-- The Wallis product $\prod_{n=1}^k \frac{2n}{2n-1}\frac{2n}{2n+1}$
  converges to `π/2` as `k → ∞` -/
lemma equality1: tendsto (λ (k : ℕ), ∏ i in Ico 1 k.succ, wallis_inside_prod i) at_top (𝓝 (π/2)) :=
begin
  rw ← tendsto_congr (aux1),
  have h : ∀ i,
  wallis_inside_prod (1 + i) = (((2 : ℝ) * i + 2) / (2 * i + 1)) * ((2 * i + 2) / (2 * i + 3)) :=
  begin
    intro i,
    rw [wallis_inside_prod, cast_add, cast_one],
    have hl : (2 : ℝ) * (1 + (i : ℝ)) / (2 * (1 + (i : ℝ)) - 1) =
      (2 * (i : ℝ) + 2) / (2 * (i : ℝ) + 1), by
    { refine congr (congr_arg has_div.div _) _; ring_nf, },
    have hr : (2 : ℝ) * (1 + (i : ℝ)) / (2 * (1 + (i : ℝ)) + 1) =
      ((2 * (i : ℝ) + 2) / (2 * (i : ℝ) + 3)), by
    { refine congr (congr_arg has_div.div _) _; ring_nf, },
    rw [hl, hr],
  end,
  have h_prod : ∀ k, ∏ (m : ℕ) in range k, wallis_inside_prod (1 + m) =
    ∏ (m : ℕ) in range k, (((2 : ℝ) * m + 2) / (2 * m + 1)) * ((2 * m + 2) / (2 * m + 3)), by
  { intro k, rw prod_congr (refl (range k)) _, intros x hx, exact h x, },
  rw tendsto_congr h_prod,
  exact tendsto_prod_pi_div_two,
end

/--
For any `n : ℕ` satisfying `n > 0` and any `r : ℝ`, we have
r * (2 * n)^2 / ((2 * n + 1) * (2 * n - 1)^2) =
r / (2* (n - 1) + 1) * 2 * n / (2 * n- 1) * 2n /(2n + 1)
-/
lemma aux2 (r : ℝ) (n : ℕ) : 1 / (((2 * n.succ + 1) : ℕ) : ℝ) *
  (r * (((((2 * n.succ) ^ 2) : ℕ ): ℝ) / ((((2 * n.succ) : ℕ) : ℝ) - 1) ^ 2)) =
  (1 / (((2 * n + 1) : ℕ) : ℝ) * r) * ((((2 * n.succ) : ℕ) : ℝ) / ((((2 * n.succ) : ℕ) : ℝ) - 1) *
  ((((2 * n.succ) : ℕ) : ℝ) / (((2 * n.succ + 1) : ℕ) : ℝ))) :=
begin
  by_cases h : r = 0,
  { repeat {rw h},
    rw [zero_mul, mul_zero, mul_zero, zero_mul] },
  { have : 2 * ((n : ℝ) + 1) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero _},
    have : 2 * (n : ℝ) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero _},
    have : 2 * ((n : ℝ) + 1) - 1 ≠ 0, by {ring_nf, norm_cast, exact succ_ne_zero _},
    field_simp,
    ring_nf },
end

/-- For any `n : ℕ`, we have
$\prod_{k=1}^n \frac{2n}{2n-1}\frac{2n}{2n+1}
  = \frac{1}{2n+1} \prod_{k=1}^n \frac{(2k)^2}{(2*k-1)^2}$
-/
lemma equation3 (n : ℕ): ∏ k in Ico 1 n.succ, wallis_inside_prod k =
  (1 : ℝ) / (2 * n + 1) * ∏ k in Ico 1 n.succ, ((2 : ℝ) * k) ^ 2 / (2 * k - 1) ^ 2 :=
begin
  induction n with d hd,
  { simp only [Ico_self, prod_empty, cast_zero, mul_zero,
    zero_add, div_one, mul_one] },
  { rw [succ_eq_add_one],
    norm_cast,
    rw [prod_Ico_succ_top, hd, wallis_inside_prod],
    symmetry,
    rw prod_Ico_succ_top,
    {norm_cast,rw aux2, },
    all_goals {apply zero_lt_succ} },
end

/--  For any `n : ℕ` with `n ≠ 0`, we have
`(2* n)^2 / (2*n - 1)^2 = (2 * n)^2 / (2 * n - 1)^2*(2*n)^2 / (2*n)^2` -/
lemma equation4 (n : ℕ) (hn : n ≠ 0) : ((2 : ℝ) * n) ^ 2 / (2 * n - 1) ^ 2 =
  ((2 : ℝ) * n) ^ 2 / (2 * n - 1) ^ 2 * ((2 * n) ^ 2 / (2 * n) ^ 2) :=
begin
  have h : ((2 : ℝ) * n) ^ 2 ≠ 0,
    from pow_ne_zero 2 (mul_ne_zero two_ne_zero (cast_ne_zero.mpr hn)),
  rw div_self h, rw mul_one,
end

/--
For any `n : ℕ`, we have
`1/(2n+1)*∏_{k=1}^n (2k)^2/(2k-1)^2 = 1/(2n+1) ∏_{k=1}^n (2k)^2/(2k-1)^2 * (2k)^2/(2k)^2`.
-/
lemma equation4' (n : ℕ) : 1 / (2 * (n : ℝ) + 1) * ∏ k in Ico 1 n.succ,
  ((2 : ℝ) * k) ^ 2 / (2 * k - 1) ^ 2 =
  1 / (2 * (n : ℝ) + 1) * ∏ k in Ico 1 n.succ,
  ((2 : ℝ) * k) ^ 2 / (2 * k - 1) ^ 2 * ((2 * k) ^ 2 / (2 * k) ^ 2) :=
begin
  rw prod_congr rfl,
  intros d hd,
  rw ← equation4,
  rw mem_Ico at hd,
  exact one_le_iff_ne_zero.mp hd.left,
end

/--
For any `n : ℕ`, we have
`(2n)^2/(2n-1)^2 * (2n)^2/(2n)^2 = 2^4 * n^4 / ((2n-1)*(2n))^2`.
-/
lemma equation5 (n : ℕ) : ((2 : ℝ) * n) ^ 2 / (2 * n - 1) ^ 2 * ((2 * n) ^ 2 / (2 * n) ^ 2) =
  ((2 : ℝ) ^ 4 * n ^ 4) / ((2 * n - 1) * (2 * n)) ^ 2 :=
begin
  cases n with d hd,
  { rw [cast_zero, mul_zero, zero_pow two_pos, zero_div, zero_mul],
    rw [zero_pow four_pos, mul_zero, zero_div], },
  { have : 2 * (d.succ : ℝ) - 1 ≠ 0, by
    { rw [cast_succ], ring_nf, norm_cast, exact succ_ne_zero (2*d), },
    have : (d.succ : ℝ) ≠ 0 := cast_ne_zero.mpr (succ_ne_zero d),
    field_simp,
    ring_nf, },
end

/--
For any `n : ℕ`, we have
`1/(2n+1) ∏_{k=1}^n (2k)^2/(2k-1)^2*(2k)^2/(2k)^2 = 1/(2n+1) ∏_{k=1}^n 2^4 k^4/ ((2k-1)(2k))^2`.
-/
lemma equation5' (n : ℕ) : 1 / (2 * (n : ℝ) + 1) * ∏ k in Ico 1 n.succ,
  ((2 : ℝ) * k) ^ 2 / (2 * k - 1) ^ 2 * ((2 * k) ^ 2 / (2 * k) ^ 2) =
  1 / (2 * (n : ℝ) + 1) * ∏ k in Ico 1 n.succ,
  ((2 : ℝ) ^ 4 * k ^ 4) / ((2 * k - 1) * (2 * k)) ^ 2 :=
begin
  rw prod_congr rfl, intros d hd, rw ← equation5,
end

/--
For any `n : ℕ`, we have
`1/(2n+1) ∏_{k=1}^n 2^4 k^4/ ((2k-1)(2k))^2 = 2^(4n)*(n!)^4/((2n)!^2 *(2n+1))` .
-/
lemma equation6 (n : ℕ) : 1 / ((2 : ℝ) * n + 1) * ∏ (k : ℕ) in Ico 1 n.succ,
  (2 : ℝ) ^ 4 * k ^ 4 / ((2 * k - 1) * (2 * k)) ^ 2 =
  (2 : ℝ) ^ (4 * n) * n.factorial ^ 4 / ((2 * n).factorial ^ 2 * (2 * n + 1)) :=
begin
  induction n with d hd,
  { rw [Ico_self, prod_empty, cast_zero, mul_zero, mul_zero, mul_zero, factorial_zero],
    rw [zero_add, pow_zero, cast_one, one_pow, one_pow, mul_one, mul_one] },
  { replace hd := congr_arg (has_mul.mul (2* (d : ℝ) + 1)) hd,
    have : 2 * (d : ℝ) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2 * d)},
    rw [← mul_assoc, mul_one_div_cancel this, one_mul] at hd,
    rw [prod_Ico_succ_top (succ_le_succ (zero_le d)), hd, mul_succ 2],
    repeat {rw factorial_succ},
    have : 2 * (d : ℝ) + 1 + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2 * d + 1)},
    have : 2 * (d.succ : ℝ) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2 * d.succ)},
    have : 2 * ((d : ℝ) + 1) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2 * (d + 1))},
    have : ((2 * d).factorial : ℝ) ≠ 0, by {norm_cast, exact factorial_ne_zero (2 * d)},
    have : 2 * ((d : ℝ) + 1) - 1 ≠ 0, by {ring_nf, norm_cast, exact succ_ne_zero (2 * d)},
    have : 2 * ((d : ℝ) + 1) ≠ 0, by {norm_cast, exact mul_ne_zero two_ne_zero (succ_ne_zero d)},
    field_simp,
    rw [mul_succ 4 d, pow_add _ (4 * d) 4],
    ring_nf }, --this one might be quite heavy without "generalize" before
end

/-- For `n : ℕ`, define `wn n` as `2^(4*n) * n!^4 / ((2*n)!^2 * (2*n + 1))` -/
noncomputable def wn (n : ℕ) : ℝ :=
  ((2 : ℝ) ^ (4 * n) * (n.factorial) ^ 4) / ((((2 * n).factorial) ^ 2) * (2 * (n : ℝ) + 1))

/-- The sequence `wn n`converges to `π/2`-/
lemma wallis_consequence : tendsto (λ (n : ℕ), wn n) at_top (𝓝 (π/2)) :=
begin
  convert equality1,
  simp only [equation6, equation3, wn, equation4', equation5', wn],
end

/--
If a sequence  `an` has a limit `A`, then the subsequence of only even terms has the same limit
-/
lemma sub_seq_tendsto {an : ℕ → ℝ} {A : ℝ} (h : tendsto an at_top (𝓝 A)) :
  tendsto (λ (n : ℕ), an (2 * n)) at_top (𝓝 A) :=
h.comp (tendsto_id.const_mul_at_top' two_pos)

/-- For `n : ℕ`, define `cn n` as √2n * (n/e)^(4n) *2^(4n) / ((√4n (2n/e)^(2n))^2 * (2n+1)) -/
noncomputable def cn (n : ℕ) : ℝ := ((sqrt (2 * n) * ((n / (exp 1)) ^ n)) ^ 4) * 2 ^ (4 * n) /
  (((sqrt (4 * n) * (((2 * n) / (exp 1))) ^ (2 * n))) ^ 2 * (2 * n + 1))

/-- For any `n :ℕ`, we have `cn n` = n/(2n+1)-/
lemma rest_cancel (n : ℕ) : (n : ℝ) / (2 * n + 1) = cn n :=
begin
  rw cn,
  have h₀ : 4 = 2 * 2, by refl,
  rw [mul_pow, mul_pow, h₀, pow_mul, sq_sqrt, sq_sqrt],
  { cases n,
    { rw [cast_zero, zero_div, mul_zero, zero_pow, zero_mul, zero_mul, zero_div],
    exact two_pos },
    { have h₁ : 2 * (n.succ : ℝ) + 1 ≠ 0,
    by { norm_cast, exact succ_ne_zero (2*n.succ) },
    have h₂ : exp 1 ≠ 0, from exp_ne_zero 1,
    have h₃ : (n.succ : ℝ) ≠ 0, by exact cast_ne_zero.mpr (succ_ne_zero n),
    field_simp,
    repeat {rw [← pow_mul]},
    rw [← h₀, mul_assoc 2 n.succ 2, mul_left_comm 2 n.succ 2, ← h₀],
    rw [mul_pow (2 : ℝ) _ (n.succ * 4), mul_comm 4 n.succ],
    ring_nf }, },
  all_goals {norm_cast, linarith},
end

/-- The sequence `cn n` has limit `1/2`-/
lemma rest_has_limit_one_half : tendsto (λ (n : ℕ), cn n) at_top (𝓝 (1 / 2)) :=
begin
  apply (tendsto.congr rest_cancel),
  have h : tendsto (λ (k : ℕ), (((k : ℝ) / (2 * (k : ℝ) + 1))⁻¹))
    at_top (𝓝 (((1 : ℝ) / 2))⁻¹) :=
  begin
    have hsucc : tendsto (λ (k : ℕ), (((k.succ : ℝ) / (2 * (k.succ : ℝ) + 1))⁻¹)) at_top
      (𝓝 (((1 : ℝ) / 2))⁻¹) :=
    begin
      have hx : ∀ (k : ℕ), (2 : ℝ) + k.succ⁻¹ = ((k.succ : ℝ) / (2 * k.succ + 1))⁻¹, by
      { intro k, have hxne : (k.succ : ℝ) ≠ 0 := nonzero_of_invertible (k.succ : ℝ), field_simp, },
      simp only [one_div, inv_inv],
      apply (tendsto.congr hx),
      have g := tendsto.add tendsto_const_nhds ((tendsto_add_at_top_iff_nat 1).mpr
        (tendsto_inverse_at_top_nhds_0_nat)),
      rw [add_zero] at g,
      exact g,
    end,
    exact (tendsto_add_at_top_iff_nat 1).mp hsucc,
  end,
  have h2: ((1 : ℝ) / 2)⁻¹ ≠ 0, by
    simp only [one_div, inv_inv, ne.def, bit0_eq_zero, one_ne_zero, not_false_iff],
  convert tendsto.inv₀ h h2,
  { simp only [inv_inv, one_div] },
  { rw inv_inv },
end

/--
Suppose the sequence `an` (defined above) has a nonzero limit `a ≠ 0`.
Then the sequence `1/ (an n)^2` has the limit `1/a^2`.
-/
lemma an_aux3 (a : ℝ) (hane : a ≠ 0) (ha : tendsto (λ (n : ℕ), an n) at_top (𝓝 a)) :
  tendsto (λ (n : ℕ), (1 / (an n)) ^ 2) at_top (𝓝 ((1 / a) ^ 2)) :=
begin
 convert tendsto.pow (tendsto.congr (λ n, (one_div (an n)).symm) (tendsto.inv₀ ha hane)) 2,
 rw [one_div],
end

/-- For any `n ≠ 0`, we have the identity `(an n)^4/ (an (2n))^2 * (cn n) = wn n`. -/
lemma expand_in_limit (n : ℕ) (hn : n ≠ 0) : (an n) ^ 4 * (1 / (an (2 * n))) ^ 2 * cn n = wn n :=
begin
  rw [an, an, cn, wn],
  have : (4 : ℝ) = (2 : ℝ) * 2, by norm_cast,
  rw this,
  rw [cast_mul 2 n, cast_two, ←mul_assoc],
  rw sqrt_mul (mul_self_nonneg 2) (n : ℝ),
  rw sqrt_mul_self zero_le_two,
  have h₀ : (n : ℝ) ≠ 0, from cast_ne_zero.mpr hn,
  have h₁ : sqrt (2 * (n : ℝ)) ≠ 0, from (ne_of_lt (zero_lt_sqrt_two_n n hn)).symm,
  have h₂ : (exp 1) ≠ 0, from exp_ne_zero 1,
  have h₃ : ((2 * n).factorial : ℝ) ≠ 0, from cast_ne_zero.mpr (factorial_ne_zero (2 * n)),
  have h₄ : sqrt (n : ℝ) ≠ 0, from sqrt_ne_zero'.mpr (cast_pos.mpr (zero_lt_iff.mpr hn)),
  have h₅ : (((2 * n) : ℕ) : ℝ) ≠ 0,
    from cast_ne_zero.mpr (mul_ne_zero two_ne_zero hn),
  have h₆ : sqrt (4 * (n : ℝ)) ≠ 0,
    from sqrt_ne_zero'.mpr (mul_pos four_pos (cast_pos.mpr (zero_lt_iff.mpr hn))),
  have h₇ : 2 * (n : ℝ) + 1 ≠ 0, by {norm_cast, exact succ_ne_zero (2*n)},
  field_simp,
  ring_nf,
end

/-- For any `n : ℕ`, we have the identity (an n+1)^4/ (an (2(n+1)))^2 * (cn n+1) = wn n+1. -/
lemma expand_in_limit' (n : ℕ) :
  (an n.succ) ^ 4 * (1 / (an (2 * n.succ))) ^ 2 * cn n.succ = wn n.succ :=
  expand_in_limit n.succ (succ_ne_zero n)

/--
Suppose the sequence `an` (defined above) has the limit `a ≠ 0`.
Then the sequence `wn` has limit `a^2/2`
-/
lemma second_wallis_limit (a : ℝ) (hane : a ≠ 0) (ha : tendsto an at_top (𝓝 a)) :
  tendsto wn at_top (𝓝 (a ^ 2 / 2)):=
begin
  rw tendsto_succ wn (a ^ 2 / 2),
  apply tendsto.congr expand_in_limit',
  let qn := λ (n : ℕ), an n ^ 4 * (1 / an (2 * n)) ^ 2 * cn n,
  have hqn :
    ∀ (n : ℕ), qn n.succ = an n.succ ^ 4 * (1 / an (2 * n.succ)) ^ 2 * cn n.succ := by tauto,
  apply tendsto.congr hqn,
  rw ←tendsto_succ qn (a ^ 2 / 2),
  have has : tendsto (λ (n : ℕ), an n ^ 4 * (1 / an (2 * n)) ^ 2) at_top (𝓝 (a ^ 2)) :=
  begin
    convert tendsto.mul (tendsto.pow ha 4) (sub_seq_tendsto (an_aux3 a hane ha)),
    field_simp,
    ring_nf,
  end,
  convert tendsto.mul has rest_has_limit_one_half,
  rw [one_div, div_eq_mul_inv],
end

/-- Stirling's Formula -/
lemma an_has_limit_sqrt_pi : tendsto (λ (n : ℕ), an n) at_top (𝓝 (sqrt π)) :=
begin
  have ha := an_has_pos_limit_a,
  cases ha with a ha,
  cases ha with hapos halimit,
  have hπ : π / 2 = a ^ 2 / 2 := tendsto_nhds_unique wallis_consequence
    (second_wallis_limit a (ne_of_gt hapos) halimit),
  field_simp at hπ,
  rw ← (sq_sqrt (le_of_lt pi_pos)) at hπ,
  have h := (sq_eq_sq (sqrt_nonneg π) (le_of_lt hapos)).mp hπ,
  convert halimit,
end

end stirling

repo: stirling


text:
import ring_theory.local_properties
import for_mathlib.localized_module

section module

variables {R X Y : Type*} [comm_ring R]
variable (M : submonoid R)
variables [add_comm_group X] [module R X] [add_comm_group Y] [module R Y] (g : X →ₗ[R] Y)

lemma submodule.le_of_localization_maximal (M M' : submodule R X)
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI M.localize J.prime_compl ≤ M'.localize J.prime_compl) : M ≤ M' :=
begin
  intros x hx,
  by_contradiction hx',
  have : (submodule.span R {M'.mkq x}).annihilator ≠ ⊤,
  { rwa [ne.def, submodule.annihilator_eq_top_iff, submodule.span_singleton_eq_bot,
      ← linear_map.mem_ker, submodule.ker_mkq] },
  obtain ⟨p, hp₁, hp₂⟩ := ideal.exists_le_maximal _ this,
  specialize H p hp₁,
  obtain ⟨y, hy, ⟨s, hs⟩, e⟩ := H (submodule.mem_localize_of_mem hx 1),
  obtain ⟨⟨u, hu⟩, e⟩ := localized_module.mk_eq.mp e,
  simp only [submonoid.smul_def, one_smul, smul_zero, subtype.coe_mk, @eq_comm X 0] at e,
  exact (mul_mem hu hs) (hp₂ $ by { rw [submodule.mem_annihilator_span_singleton, ← M'.mkq.map_smul,
    ← linear_map.mem_ker, submodule.ker_mkq, mul_smul, e], exact M'.smul_mem _ hy })
end

lemma submodule.eq_of_localization_maximal (M M' : submodule R X)
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI M.localize J.prime_compl = M'.localize J.prime_compl) : M = M' :=
(submodule.le_of_localization_maximal _ _ $ by simp [H]).antisymm
  (submodule.le_of_localization_maximal _ _ $ by simp [H])

lemma submodule.eq_bot_of_localization_maximal (M : submodule R X)
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI M.localize J.prime_compl = ⊥) : M = ⊥ :=
submodule.eq_of_localization_maximal _ _ (by simp [H])

lemma submodule.eq_top_of_localization_maximal (M : submodule R X)
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI M.localize J.prime_compl = ⊤) : M = ⊤ :=
submodule.eq_of_localization_maximal _ _ (by simp [H])

lemma module.subsingleton_of_localization_maximal (X : Type*) [add_comm_group X] [module R X]
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI subsingleton (localized_module J.prime_compl X)) : subsingleton X :=
begin
  simp_rw [← submodule.subsingleton_iff R, ← subsingleton_iff_bot_eq_top, @eq_comm _ ⊥] at ⊢,
  apply submodule.eq_bot_of_localization_maximal,
  exact λ J hJ, subsingleton.elim _ _
end

lemma module.eq_zero_of_localization_maximal (x : X)
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI localized_module.mk x (1 : J.prime_compl) = 0) : x = 0 :=
begin
  rw ← @submodule.span_singleton_eq_bot R,
  apply submodule.eq_bot_of_localization_maximal,
  simp_rw [submodule.localize_eq_span, submodule.map_span, set.image_singleton,
    submodule.span_span_of_tower, submodule.span_singleton_eq_bot],
  exact H
end

include g

lemma linear_map.injective_of_localization_maximal
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI function.injective (localized_module.map J.prime_compl g)) : function.injective g :=
begin
  rw ← linear_map.ker_eq_bot,
  apply submodule.eq_bot_of_localization_maximal,
  introsI J hJ,
  rw [linear_map.ker, ← submodule.localize_comap_map, submodule.localize_bot, submodule.comap_bot,
    linear_map.ker_eq_bot],
  exact H J hJ
end

lemma linear_map.surjective_of_localization_maximal
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI function.surjective (localized_module.map J.prime_compl g)) : function.surjective g :=
begin
  rw ← linear_map.range_eq_top,
  apply submodule.eq_top_of_localization_maximal,
  introsI J hJ,
  rw [linear_map.range_eq_map, ← submodule.localize_map_map, submodule.localize_top,
    submodule.map_top, linear_map.range_eq_top],
  exact H J hJ
end

lemma linear_map.bijective_of_localization_maximal
  (H : ∀ (J : ideal R) (hJ : J.is_maximal),
    by exactI function.bijective (localized_module.map J.prime_compl g)) : function.bijective g :=
⟨linear_map.injective_of_localization_maximal g (λ J hJ, (H J hJ).1),
  linear_map.surjective_of_localization_maximal g (λ J hJ, (H J hJ).2)⟩

lemma linear_map.injective_localized_module_map (h : function.injective g) :
  function.injective (localized_module.map M g) :=
by rw [← linear_map.ker_eq_bot, linear_map.ker, ← submodule.localize_bot M,
  submodule.localize_comap_map, submodule.comap_bot, linear_map.ker_eq_bot.mpr h,
  submodule.localize_bot]

lemma linear_map.surjective_localized_module_map (h : function.surjective g) :
  function.surjective (localized_module.map M g) :=
by rw [← linear_map.range_eq_top, linear_map.range_eq_map, ← submodule.localize_top M,
  submodule.localize_map_map, submodule.map_top, linear_map.range_eq_top.mpr h,
  submodule.localize_top]

lemma linear_map.bijective_localized_module_map (h : function.bijective g) :
  function.bijective (localized_module.map M g) :=
⟨linear_map.injective_localized_module_map M g h.1,
  linear_map.surjective_localized_module_map M g h.2⟩

end module

author: erdOne

repo: lean-AG-morphisms


text:
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Mario Carneiro

Denumerable (countably infinite) types, as a typeclass extending
encodable. This is used to provide explicit encode/decode functions
from nat, where the functions are known inverses of each other.
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.data.equiv.encodable.basic
import Mathlib.data.sigma.default
import Mathlib.data.fintype.basic
import Mathlib.data.list.min_max
import Mathlib.PostPort

universes u_1 l u_2 u_3

namespace Mathlib

/-- A denumerable type is one which is (constructively) bijective with ℕ.
  Although we already have a name for this property, namely `α ≃ ℕ`,
  we are here interested in using it as a typeclass. -/
class denumerable (α : Type u_1)
extends encodable α
where
  decode_inv : ∀ (n : ℕ), ∃ (a : α), ∃ (H : a ∈ encodable.decode α n), encodable.encode a = n

namespace denumerable

theorem decode_is_some (α : Type u_1) [denumerable α] (n : ℕ) : ↥(option.is_some (encodable.decode α n)) :=
  iff.mpr option.is_some_iff_exists (Exists.imp (fun (a : α) => Exists.fst) (decode_inv n))

def of_nat (α : Type u_1) [f : denumerable α] (n : ℕ) : α :=
  option.get (decode_is_some α n)

@[simp] theorem decode_eq_of_nat (α : Type u_1) [denumerable α] (n : ℕ) : encodable.decode α n = some (of_nat α n) :=
  option.eq_some_of_is_some (decode_is_some α n)

@[simp] theorem of_nat_of_decode {α : Type u_1} [denumerable α] {n : ℕ} {b : α} (h : encodable.decode α n = some b) : of_nat α n = b :=
  option.some.inj (Eq.trans (Eq.symm (decode_eq_of_nat α n)) h)

@[simp] theorem encode_of_nat {α : Type u_1} [denumerable α] (n : ℕ) : encodable.encode (of_nat α n) = n := sorry

@[simp] theorem of_nat_encode {α : Type u_1} [denumerable α] (a : α) : of_nat α (encodable.encode a) = a :=
  of_nat_of_decode (encodable.encodek a)

def eqv (α : Type u_1) [denumerable α] : α ≃ ℕ :=
  equiv.mk encodable.encode (of_nat α) of_nat_encode encode_of_nat

def mk' {α : Type u_1} (e : α ≃ ℕ) : denumerable α :=
  mk sorry

def of_equiv (α : Type u_1) {β : Type u_2} [denumerable α] (e : β ≃ α) : denumerable β :=
  mk sorry

@[simp] theorem of_equiv_of_nat (α : Type u_1) {β : Type u_2} [denumerable α] (e : β ≃ α) (n : ℕ) : of_nat β n = coe_fn (equiv.symm e) (of_nat α n) := sorry

def equiv₂ (α : Type u_1) (β : Type u_2) [denumerable α] [denumerable β] : α ≃ β :=
  equiv.trans (eqv α) (equiv.symm (eqv β))

protected instance nat : denumerable ℕ :=
  mk sorry

@[simp] theorem of_nat_nat (n : ℕ) : of_nat ℕ n = n :=
  rfl

protected instance option {α : Type u_1} [denumerable α] : denumerable (Option α) :=
  mk sorry

protected instance sum {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] : denumerable (α ⊕ β) :=
  mk sorry

protected instance sigma {α : Type u_1} [denumerable α] {γ : α → Type u_3} [(a : α) → denumerable (γ a)] : denumerable (sigma γ) :=
  mk sorry

@[simp] theorem sigma_of_nat_val {α : Type u_1} [denumerable α] {γ : α → Type u_3} [(a : α) → denumerable (γ a)] (n : ℕ) : of_nat (sigma γ) n =
  sigma.mk (of_nat α (prod.fst (nat.unpair n)))
    (of_nat (γ (of_nat α (prod.fst (nat.unpair n)))) (prod.snd (nat.unpair n))) := sorry

protected instance prod {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] : denumerable (α × β) :=
  of_equiv (sigma fun (_x : α) => β) (equiv.symm (equiv.sigma_equiv_prod α β))

@[simp] theorem prod_of_nat_val {α : Type u_1} {β : Type u_2} [denumerable α] [denumerable β] (n : ℕ) : of_nat (α × β) n = (of_nat α (prod.fst (nat.unpair n)), of_nat β (prod.snd (nat.unpair n))) := sorry

@[simp] theorem prod_nat_of_nat : of_nat (ℕ × ℕ) = nat.unpair := sorry

protected instance int : denumerable ℤ :=
  mk' equiv.int_equiv_nat

protected instance pnat : denumerable ℕ+ :=
  mk' equiv.pnat_equiv_nat

protected instance ulift {α : Type u_1} [denumerable α] : denumerable (ulift α) :=
  of_equiv α equiv.ulift

protected instance plift {α : Type u_1} [denumerable α] : denumerable (plift α) :=
  of_equiv α equiv.plift

def pair {α : Type u_1} [denumerable α] : α × α ≃ α :=
  equiv₂ (α × α) α

end denumerable

namespace nat.subtype

theorem exists_succ {s : set ℕ} [infinite ↥s] (x : ↥s) : ∃ (n : ℕ), subtype.val x + n + 1 ∈ s := sorry

def succ {s : set ℕ} [infinite ↥s] [decidable_pred s] (x : ↥s) : ↥s :=
  (fun (h : ∃ (m : ℕ), subtype.val x + m + 1 ∈ s) => { val := subtype.val x + nat.find h + 1, property := sorry })
    (exists_succ x)

theorem succ_le_of_lt {s : set ℕ} [infinite ↥s] [decidable_pred s] {x : ↥s} {y : ↥s} (h : y < x) : succ y ≤ x := sorry

theorem le_succ_of_forall_lt_le {s : set ℕ} [infinite ↥s] [decidable_pred s] {x : ↥s} {y : ↥s} (h : ∀ (z : ↥s), z < x → z ≤ y) : x ≤ succ y := sorry

theorem lt_succ_self {s : set ℕ} [infinite ↥s] [decidable_pred s] (x : ↥s) : x < succ x :=
  lt_of_le_of_lt (le_add_right (le_refl (subtype.val x))) (lt_succ_self (subtype.val x + nat.find (exists_succ x)))

theorem lt_succ_iff_le {s : set ℕ} [infinite ↥s] [decidable_pred s] {x : ↥s} {y : ↥s} : x < succ y ↔ x ≤ y :=
  { mp := fun (h : x < succ y) => le_of_not_gt fun (h' : x > y) => not_le_of_gt h (succ_le_of_lt h'),
    mpr := fun (h : x ≤ y) => lt_of_le_of_lt h (lt_succ_self y) }

def of_nat (s : set ℕ) [decidable_pred s] [infinite ↥s] : ℕ → ↥s :=
  sorry

theorem of_nat_surjective_aux {s : set ℕ} [infinite ↥s] [decidable_pred s] {x : ℕ} (hx : x ∈ s) : ∃ (n : ℕ), of_nat s n = { val := x, property := hx } := sorry

theorem of_nat_surjective {s : set ℕ} [infinite ↥s] [decidable_pred s] : function.surjective (of_nat s) := sorry

def denumerable (s : set ℕ) [decidable_pred s] [infinite ↥s] : denumerable ↥s :=
  denumerable.of_equiv ℕ (equiv.mk to_fun_aux (of_nat s) sorry sorry)

end nat.subtype

namespace denumerable

def of_encodable_of_infinite (α : Type u_1) [encodable α] [infinite α] : denumerable α :=
  let _inst : decidable_pred (set.range encodable.encode) := encodable.decidable_range_encode α;
  let _inst_3 : infinite ↥(set.range encodable.encode) := sorry;
  let _inst_4 : denumerable ↥(set.range encodable.encode) := nat.subtype.denumerable (set.range encodable.encode);
  of_equiv (↥(set.range encodable.encode)) (encodable.equiv_range_encode α)

author: AurelienSaue


text:
/-
Copyright (c) 2019 Abhimanyu Pallavi Sudhir. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Abhimanyu Pallavi Sudhir
-/
import order.filter.filter_product
import analysis.specific_limits

/-!
# Construction of the hyperreal numbers as an ultraproduct of real sequences.
-/

open filter filter.germ
open_locale topological_space classical

/-- Hyperreal numbers on the ultrafilter extending the cofinite filter -/
@[derive [linear_ordered_field, inhabited]]
def hyperreal : Type := germ (hyperfilter ℕ : filter ℕ) ℝ

namespace hyperreal

notation `ℝ*` := hyperreal

noncomputable instance : has_coe_t ℝ ℝ* := ⟨λ x, (↑x : germ _ _)⟩

@[simp, norm_cast]
lemma coe_eq_coe {x y : ℝ} : (x : ℝ*) = y ↔ x = y :=
germ.const_inj

@[simp, norm_cast] lemma coe_eq_zero {x : ℝ} : (x : ℝ*) = 0 ↔ x = 0 := coe_eq_coe
@[simp, norm_cast] lemma coe_eq_one {x : ℝ} : (x : ℝ*) = 1 ↔ x = 1 := coe_eq_coe

@[simp, norm_cast] lemma coe_one : ↑(1 : ℝ) = (1 : ℝ*) := rfl
@[simp, norm_cast] lemma coe_zero : ↑(0 : ℝ) = (0 : ℝ*) := rfl
@[simp, norm_cast] lemma coe_inv (x : ℝ) : ↑(x⁻¹) = (x⁻¹ : ℝ*) := rfl
@[simp, norm_cast] lemma coe_neg (x : ℝ) : ↑(-x) = (-x : ℝ*) := rfl
@[simp, norm_cast] lemma coe_add (x y : ℝ) : ↑(x + y) = (x + y : ℝ*) := rfl
@[simp, norm_cast] lemma coe_bit0 (x : ℝ) : ↑(bit0 x) = (bit0 x : ℝ*) := rfl
@[simp, norm_cast] lemma coe_bit1 (x : ℝ) : ↑(bit1 x) = (bit1 x : ℝ*) := rfl
@[simp, norm_cast] lemma coe_mul (x y : ℝ) : ↑(x * y) = (x * y : ℝ*) := rfl
@[simp, norm_cast] lemma coe_div (x y : ℝ) : ↑(x / y) = (x / y : ℝ*) := rfl
@[simp, norm_cast] lemma coe_sub (x y : ℝ) : ↑(x - y) = (x - y : ℝ*) := rfl

@[simp, norm_cast] lemma coe_lt_coe {x y : ℝ} : (x : ℝ*) < y ↔ x < y := germ.const_lt
@[simp, norm_cast] lemma coe_pos {x : ℝ} : 0 < (x : ℝ*) ↔ 0 < x :=
coe_lt_coe
@[simp, norm_cast] lemma coe_le_coe {x y : ℝ} : (x : ℝ*) ≤ y ↔ x ≤ y := germ.const_le_iff
@[simp, norm_cast] lemma coe_abs (x : ℝ) : ((|x| : ℝ) : ℝ*) = |x| :=
begin
  convert const_abs x,
  apply lattice_of_linear_order_eq_filter_germ_lattice,
end
@[simp, norm_cast] lemma coe_max (x y : ℝ) : ((max x y : ℝ) : ℝ*) = max x y := germ.const_max _ _
@[simp, norm_cast] lemma coe_min (x y : ℝ) : ((min x y : ℝ) : ℝ*) = min x y := germ.const_min _ _

/-- Construct a hyperreal number from a sequence of real numbers. -/
noncomputable def of_seq (f : ℕ → ℝ) : ℝ* := (↑f : germ (hyperfilter ℕ : filter ℕ) ℝ)

/-- A sample infinitesimal hyperreal-/
noncomputable def epsilon : ℝ* := of_seq $ λ n, n⁻¹

/-- A sample infinite hyperreal-/
noncomputable def omega : ℝ* := of_seq coe

localized "notation `ε` := hyperreal.epsilon" in hyperreal
localized "notation `ω` := hyperreal.omega" in hyperreal

lemma epsilon_eq_inv_omega : ε = ω⁻¹ := rfl

lemma inv_epsilon_eq_omega : ε⁻¹ = ω := @inv_inv₀ _ _ ω

lemma epsilon_pos : 0 < ε :=
suffices ∀ᶠ i in hyperfilter ℕ, (0 : ℝ) < (i : ℕ)⁻¹, by rwa lt_def,
have h0' : {n : ℕ | ¬ 0 < n} = {0} :=
by simp only [not_lt, (set.set_of_eq_eq_singleton).symm]; ext; exact nat.le_zero_iff,
begin
  simp only [inv_pos, nat.cast_pos],
  exact mem_hyperfilter_of_finite_compl (by convert set.finite_singleton _),
end

lemma epsilon_ne_zero : ε ≠ 0 := ne_of_gt epsilon_pos

lemma omega_pos : 0 < ω := by rw ←inv_epsilon_eq_omega; exact inv_pos.2 epsilon_pos

lemma omega_ne_zero : ω ≠ 0 := ne_of_gt omega_pos

theorem epsilon_mul_omega : ε * ω = 1 := @inv_mul_cancel _ _ ω omega_ne_zero

lemma lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
  ∀ {r : ℝ}, 0 < r → of_seq f < (r : ℝ*) :=
begin
  simp only [metric.tendsto_at_top, dist_zero_right, norm, lt_def] at hf ⊢,
  intros r hr, cases hf r hr with N hf',
  have hs : {i : ℕ | f i < r}ᶜ ⊆ {i : ℕ | i ≤ N} :=
    λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
    exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
  exact mem_hyperfilter_of_finite_compl
    ((set.finite_le_nat N).subset hs)
end

lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
  ∀ {r : ℝ}, 0 < r → (-r : ℝ*) < of_seq f :=
λ r hr, have hg : _ := hf.neg,
neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)

lemma gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
  ∀ {r : ℝ}, r < 0 → (r : ℝ*) < of_seq f :=
λ r hr, by rw [←neg_neg r, coe_neg];
exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

lemma epsilon_lt_pos (x : ℝ) : 0 < x → ε < x :=
lt_of_tendsto_zero_of_pos tendsto_inverse_at_top_nhds_0_nat

/-- Standard part predicate -/
def is_st (x : ℝ*) (r : ℝ) := ∀ δ : ℝ, 0 < δ → (r - δ : ℝ*) < x ∧ x < r + δ

/-- Standard part function: like a "round" to ℝ instead of ℤ -/
noncomputable def st : ℝ* → ℝ :=
λ x, if h : ∃ r, is_st x r then classical.some h else 0

/-- A hyperreal number is infinitesimal if its standard part is 0 -/
def infinitesimal (x : ℝ*) := is_st x 0

/-- A hyperreal number is positive infinite if it is larger than all real numbers -/
def infinite_pos (x : ℝ*) := ∀ r : ℝ, ↑r < x

/-- A hyperreal number is negative infinite if it is smaller than all real numbers -/
def infinite_neg (x : ℝ*) := ∀ r : ℝ, x < r

/-- A hyperreal number is infinite if it is infinite positive or infinite negative -/
def infinite (x : ℝ*) := infinite_pos x ∨ infinite_neg x

/-!
### Some facts about `st`
-/

private lemma is_st_unique' (x : ℝ*) (r s : ℝ) (hr : is_st x r) (hs : is_st x s) (hrs : r < s) :
  false :=
have hrs' : _ := half_pos $ sub_pos_of_lt hrs,
have hr' : _ := (hr _ hrs').2,
have hs' : _ := (hs _ hrs').1,
have h : s - ((s - r) / 2) = r + (s - r) / 2 := by linarith,
begin
  norm_cast at *,
  rw h at hs',
  exact not_lt_of_lt hs' hr'
end

theorem is_st_unique {x : ℝ*} {r s : ℝ} (hr : is_st x r) (hs : is_st x s) : r = s :=
begin
  rcases lt_trichotomy r s with h | h | h,
  { exact false.elim (is_st_unique' x r s hr hs h) },
  { exact h },
  { exact false.elim (is_st_unique' x s r hs hr h) }
end

theorem not_infinite_of_exists_st {x : ℝ*} : (∃ r : ℝ, is_st x r) → ¬ infinite x :=
λ he hi, Exists.dcases_on he $ λ r hr, hi.elim
   (λ hip, not_lt_of_lt (hr 2 zero_lt_two).2 (hip $ r + 2))
   (λ hin, not_lt_of_lt (hr 2 zero_lt_two).1 (hin $ r - 2))

theorem is_st_Sup {x : ℝ*} (hni : ¬ infinite x) : is_st x (Sup {y : ℝ | (y : ℝ*) < x}) :=
let S : set ℝ := {y : ℝ | (y : ℝ*) < x} in
let R : _ := Sup S in
have hnile : _ := not_forall.mp (not_or_distrib.mp hni).1,
have hnige : _ := not_forall.mp (not_or_distrib.mp hni).2,
Exists.dcases_on hnile $ Exists.dcases_on hnige $ λ r₁ hr₁ r₂ hr₂,
have HR₁ : S.nonempty :=
  ⟨r₁ - 1, lt_of_lt_of_le (coe_lt_coe.2 $ sub_one_lt _) (not_lt.mp hr₁) ⟩,
have HR₂ : bdd_above S :=
  ⟨ r₂, λ y hy, le_of_lt (coe_lt_coe.1 (lt_of_lt_of_le hy (not_lt.mp hr₂))) ⟩,
λ δ hδ,
  ⟨ lt_of_not_ge' $ λ c,
      have hc : ∀ y ∈ S, y ≤ R - δ := λ y hy, coe_le_coe.1 $ le_of_lt $ lt_of_lt_of_le hy c,
      not_lt_of_le (cSup_le HR₁ hc) $ sub_lt_self R hδ,
    lt_of_not_ge' $ λ c,
      have hc : ↑(R + δ / 2) < x :=
        lt_of_lt_of_le (add_lt_add_left (coe_lt_coe.2 (half_lt_self hδ)) R) c,
      not_lt_of_le (le_cSup HR₂ hc) $ (lt_add_iff_pos_right _).mpr $ half_pos hδ⟩

theorem exists_st_of_not_infinite {x : ℝ*} (hni : ¬ infinite x) : ∃ r : ℝ, is_st x r :=
⟨Sup {y : ℝ | (y : ℝ*) < x}, is_st_Sup hni⟩

theorem st_eq_Sup {x : ℝ*} : st x = Sup {y : ℝ | (y : ℝ*) < x} :=
begin
unfold st, split_ifs,
{ exact is_st_unique (classical.some_spec h) (is_st_Sup (not_infinite_of_exists_st h)) },
{ cases not_imp_comm.mp exists_st_of_not_infinite h with H H,
  { rw (set.ext (λ i, ⟨λ hi, set.mem_univ i, λ hi, H i⟩) : {y : ℝ | (y : ℝ*) < x} = set.univ),
    exact real.Sup_univ.symm },
  { rw (set.ext (λ i, ⟨λ hi, false.elim (not_lt_of_lt (H i) hi),
    λ hi, false.elim (set.not_mem_empty i hi)⟩) : {y : ℝ | (y : ℝ*) < x} = ∅),
    exact real.Sup_empty.symm } }
end

theorem exists_st_iff_not_infinite {x : ℝ*} : (∃ r : ℝ, is_st x r) ↔ ¬ infinite x :=
⟨ not_infinite_of_exists_st, exists_st_of_not_infinite ⟩

theorem infinite_iff_not_exists_st {x : ℝ*} : infinite x ↔ ¬ ∃ r : ℝ, is_st x r :=
iff_not_comm.mp exists_st_iff_not_infinite

theorem st_infinite {x : ℝ*} (hi : infinite x) : st x = 0 :=
begin
  unfold st, split_ifs,
  { exact false.elim ((infinite_iff_not_exists_st.mp hi) h) },
  { refl }
end

lemma st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : st x = r :=
begin
  unfold st, split_ifs,
  { exact is_st_unique (classical.some_spec h) hxr },
  { exact false.elim (h ⟨r, hxr⟩) }
end

lemma is_st_st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st x (st x) :=
by rwa [st_of_is_st hxr]

lemma is_st_st_of_exists_st {x : ℝ*} (hx : ∃ r : ℝ, is_st x r) : is_st x (st x) :=
Exists.dcases_on hx (λ r, is_st_st_of_is_st)

lemma is_st_st {x : ℝ*} (hx : st x ≠ 0) : is_st x (st x) :=
begin
  unfold st, split_ifs,
  { exact classical.some_spec h },
  { exact false.elim (hx (by unfold st; split_ifs; refl)) }
end

lemma is_st_st' {x : ℝ*} (hx : ¬ infinite x) : is_st x (st x) :=
is_st_st_of_exists_st $ exists_st_of_not_infinite hx

lemma is_st_refl_real (r : ℝ) : is_st r r :=
λ δ hδ, ⟨ sub_lt_self _ (coe_lt_coe.2 hδ), (lt_add_of_pos_right _ (coe_lt_coe.2 hδ)) ⟩

lemma st_id_real (r : ℝ) : st r = r := st_of_is_st (is_st_refl_real r)

lemma eq_of_is_st_real {r s : ℝ} : is_st r s → r = s := is_st_unique (is_st_refl_real r)

lemma is_st_real_iff_eq {r s : ℝ} : is_st r s ↔ r = s :=
⟨eq_of_is_st_real, λ hrs, by rw [hrs]; exact is_st_refl_real s⟩

lemma is_st_symm_real {r s : ℝ} : is_st r s ↔ is_st s r :=
by rw [is_st_real_iff_eq, is_st_real_iff_eq, eq_comm]

lemma is_st_trans_real {r s t : ℝ} : is_st r s → is_st s t → is_st r t :=
by rw [is_st_real_iff_eq, is_st_real_iff_eq, is_st_real_iff_eq]; exact eq.trans

lemma is_st_inj_real {r₁ r₂ s : ℝ} (h1 : is_st r₁ s) (h2 : is_st r₂ s) : r₁ = r₂ :=
eq.trans (eq_of_is_st_real h1) (eq_of_is_st_real h2).symm

lemma is_st_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} :
  is_st x r ↔ ∀ (δ : ℝ), 0 < δ → |x - r| < δ :=
by simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, is_st, and_comm, add_comm]

lemma is_st_add {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x + y) (r + s) :=
λ hxr hys d hd,
have hxr' : _ := hxr (d / 2) (half_pos hd),
have hys' : _ := hys (d / 2) (half_pos hd),
⟨by convert add_lt_add hxr'.1 hys'.1 using 1; norm_cast; linarith,
 by convert add_lt_add hxr'.2 hys'.2 using 1; norm_cast; linarith⟩

lemma is_st_neg {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st (-x) (-r) :=
λ d hd, show -(r : ℝ*) - d < -x ∧ -x < -r + d, by cases (hxr d hd); split; linarith

lemma is_st_sub {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x - y) (r - s) :=
λ hxr hys, by rw [sub_eq_add_neg, sub_eq_add_neg]; exact is_st_add hxr (is_st_neg hys)

/- (st x < st y) → (x < y) → (x ≤ y) → (st x ≤ st y) -/

lemma lt_of_is_st_lt {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
  r < s → x < y :=
λ hrs, have hrs' : 0 < (s - r) / 2 := half_pos (sub_pos.mpr hrs),
have hxr' : _ := (hxr _ hrs').2, have hys' : _ := (hys _ hrs').1,
have H1 : r + ((s - r) / 2) = (r + s) / 2 := by linarith,
have H2 : s - ((s - r) / 2) = (r + s) / 2 := by linarith,
begin
  norm_cast at *,
  rw H1 at hxr',
  rw H2 at hys',
  exact lt_trans hxr' hys'
end

lemma is_st_le_of_le {x y : ℝ*} {r s : ℝ} (hrx : is_st x r) (hsy : is_st y s) :
  x ≤ y → r ≤ s := by rw [←not_lt, ←not_lt, not_imp_not]; exact lt_of_is_st_lt hsy hrx

lemma st_le_of_le {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
  x ≤ y → st x ≤ st y :=
have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
is_st_le_of_le hx' hy'

lemma lt_of_st_lt {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
  st x < st y → x < y :=
have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
lt_of_is_st_lt hx' hy'

/-!
### Basic lemmas about infinite
-/

lemma infinite_pos_def {x : ℝ*} : infinite_pos x ↔ ∀ r : ℝ, ↑r < x := by rw iff_eq_eq; refl

lemma infinite_neg_def {x : ℝ*} : infinite_neg x ↔ ∀ r : ℝ, x < r := by rw iff_eq_eq; refl

lemma ne_zero_of_infinite {x : ℝ*} : infinite x → x ≠ 0 :=
λ hI h0, or.cases_on hI
  (λ hip, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_pos 0) 0))
  (λ hin, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_neg 0) 0))

lemma not_infinite_zero : ¬ infinite 0 := λ hI, ne_zero_of_infinite hI rfl

lemma pos_of_infinite_pos {x : ℝ*} : infinite_pos x → 0 < x := λ hip, hip 0

lemma neg_of_infinite_neg {x : ℝ*} : infinite_neg x → x < 0 := λ hin, hin 0

lemma not_infinite_pos_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinite_pos x :=
λ hn hp, not_lt_of_lt (hn 1) (hp 1)

lemma not_infinite_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinite_neg x :=
imp_not_comm.mp not_infinite_pos_of_infinite_neg

lemma infinite_neg_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → infinite_neg (-x) :=
λ hp r, neg_lt.mp (hp (-r))

lemma infinite_pos_neg_of_infinite_neg {x : ℝ*} : infinite_neg x → infinite_pos (-x) :=
λ hp r, lt_neg.mp (hp (-r))

lemma infinite_pos_iff_infinite_neg_neg {x : ℝ*} : infinite_pos x ↔ infinite_neg (-x) :=
⟨ infinite_neg_neg_of_infinite_pos, λ hin, neg_neg x ▸ infinite_pos_neg_of_infinite_neg hin ⟩

lemma infinite_neg_iff_infinite_pos_neg {x : ℝ*} : infinite_neg x ↔ infinite_pos (-x) :=
⟨ infinite_pos_neg_of_infinite_neg, λ hin, neg_neg x ▸ infinite_neg_neg_of_infinite_pos hin ⟩

lemma infinite_iff_infinite_neg {x : ℝ*} : infinite x ↔ infinite (-x) :=
⟨ λ hi, or.cases_on hi
  (λ hip, or.inr (infinite_neg_neg_of_infinite_pos hip))
  (λ hin, or.inl (infinite_pos_neg_of_infinite_neg hin)),
 λ hi, or.cases_on hi
  (λ hipn, or.inr (infinite_neg_iff_infinite_pos_neg.mpr hipn))
  (λ hinp, or.inl (infinite_pos_iff_infinite_neg_neg.mpr hinp))⟩

lemma not_infinite_of_infinitesimal {x : ℝ*} : infinitesimal x → ¬ infinite x :=
λ hi hI, have hi' : _ := (hi 2 zero_lt_two), or.dcases_on hI
  (λ hip, have hip' : _ := hip 2, not_lt_of_lt hip' (by convert hi'.2; exact (zero_add 2).symm))
  (λ hin, have hin' : _ := hin (-2), not_lt_of_lt hin' (by convert hi'.1; exact (zero_sub 2).symm))

lemma not_infinitesimal_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinitesimal x :=
λ hp, not_infinitesimal_of_infinite (or.inl hp)

lemma not_infinitesimal_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinitesimal x :=
λ hn, not_infinitesimal_of_infinite (or.inr hn)

lemma infinite_pos_iff_infinite_and_pos {x : ℝ*} : infinite_pos x ↔ (infinite x ∧ 0 < x) :=
⟨ λ hip, ⟨or.inl hip, hip 0⟩,
  λ ⟨hi, hp⟩, hi.cases_on (λ hip, hip) (λ hin, false.elim (not_lt_of_lt hp (hin 0))) ⟩

lemma infinite_neg_iff_infinite_and_neg {x : ℝ*} : infinite_neg x ↔ (infinite x ∧ x < 0) :=
⟨ λ hip, ⟨or.inr hip, hip 0⟩,
  λ ⟨hi, hp⟩, hi.cases_on (λ hin, false.elim (not_lt_of_lt hp (hin 0))) (λ hip, hip) ⟩

lemma infinite_pos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) : infinite_pos x ↔ infinite x :=
by rw [infinite_pos_iff_infinite_and_pos]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hp⟩⟩

lemma infinite_pos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 ≤ x) : infinite_pos x ↔ infinite x :=
or.cases_on (lt_or_eq_of_le hp) (infinite_pos_iff_infinite_of_pos)
  (λ h, by rw h.symm; exact
  ⟨λ hIP, false.elim (not_infinite_zero (or.inl hIP)), λ hI, false.elim (not_infinite_zero hI)⟩)

lemma infinite_neg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) : infinite_neg x ↔ infinite x :=
by rw [infinite_neg_iff_infinite_and_neg]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hn⟩⟩

lemma infinite_pos_abs_iff_infinite_abs {x : ℝ*} : infinite_pos (|x|) ↔ infinite (|x|) :=
infinite_pos_iff_infinite_of_nonneg (abs_nonneg _)

lemma infinite_iff_infinite_pos_abs {x : ℝ*} : infinite x ↔ infinite_pos (|x|) :=
⟨ λ hi d, or.cases_on hi
   (λ hip, by rw [abs_of_pos (hip 0)]; exact hip d)
   (λ hin, by rw [abs_of_neg (hin 0)]; exact lt_neg.mp (hin (-d))),
  λ hipa, by { rcases (lt_trichotomy x 0) with h | h | h,
    { exact or.inr (infinite_neg_iff_infinite_pos_neg.mpr (by rwa abs_of_neg h at hipa)) },
    { exact false.elim (ne_zero_of_infinite (or.inl (by rw [h]; rwa [h, abs_zero] at hipa)) h) },
    { exact or.inl (by rwa abs_of_pos h at hipa) } } ⟩

lemma infinite_iff_infinite_abs {x : ℝ*} : infinite x ↔ infinite (|x|) :=
by rw [←infinite_pos_iff_infinite_of_nonneg (abs_nonneg _), infinite_iff_infinite_pos_abs]

lemma infinite_iff_abs_lt_abs {x : ℝ*} : infinite x ↔ ∀ r : ℝ, (|r| : ℝ*) < |x| :=
⟨ λ hI r, (coe_abs r) ▸ infinite_iff_infinite_pos_abs.mp hI (|r|),
  λ hR, or.cases_on (max_choice x (-x))
  (λ h, or.inl $ λ r, lt_of_le_of_lt (le_abs_self _) (h ▸ (hR r)))
  (λ h, or.inr $ λ r, neg_lt_neg_iff.mp $ lt_of_le_of_lt (neg_le_abs_self _) (h ▸ (hR r)))⟩

lemma infinite_pos_add_not_infinite_neg {x y : ℝ*} :
  infinite_pos x → ¬ infinite_neg y → infinite_pos (x + y) :=
begin
  intros hip hnin r,
  cases not_forall.mp hnin with r₂ hr₂,
  convert add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1,
  simp
end

lemma not_infinite_neg_add_infinite_pos {x y : ℝ*} :
  ¬ infinite_neg x → infinite_pos y → infinite_pos (x + y) :=
λ hx hy, by rw [add_comm]; exact infinite_pos_add_not_infinite_neg hy hx

lemma infinite_neg_add_not_infinite_pos {x y : ℝ*} :
  infinite_neg x → ¬ infinite_pos y → infinite_neg (x + y) :=
by rw [@infinite_neg_iff_infinite_pos_neg x, @infinite_pos_iff_infinite_neg_neg y,
       @infinite_neg_iff_infinite_pos_neg (x + y), neg_add];
exact infinite_pos_add_not_infinite_neg

lemma not_infinite_pos_add_infinite_neg {x y : ℝ*} :
  ¬ infinite_pos x → infinite_neg y → infinite_neg (x + y) :=
λ hx hy, by rw [add_comm]; exact infinite_neg_add_not_infinite_pos hy hx

lemma infinite_pos_add_infinite_pos {x y : ℝ*} :
  infinite_pos x → infinite_pos y → infinite_pos (x + y) :=
λ hx hy, infinite_pos_add_not_infinite_neg hx (not_infinite_neg_of_infinite_pos hy)

lemma infinite_neg_add_infinite_neg {x y : ℝ*} :
  infinite_neg x → infinite_neg y → infinite_neg (x + y) :=
λ hx hy, infinite_neg_add_not_infinite_pos hx (not_infinite_pos_of_infinite_neg hy)

lemma infinite_pos_add_not_infinite {x y : ℝ*} :
  infinite_pos x → ¬ infinite y → infinite_pos (x + y) :=
λ hx hy, infinite_pos_add_not_infinite_neg hx (not_or_distrib.mp hy).2

lemma infinite_neg_add_not_infinite {x y : ℝ*} :
  infinite_neg x → ¬ infinite y → infinite_neg (x + y) :=
λ hx hy, infinite_neg_add_not_infinite_pos hx (not_or_distrib.mp hy).1

theorem infinite_pos_of_tendsto_top {f : ℕ → ℝ} (hf : tendsto f at_top at_top) :
  infinite_pos (of_seq f) :=
λ r, have hf' : _ := tendsto_at_top_at_top.mp hf,
Exists.cases_on (hf' (r + 1)) $ λ i hi,
  have hi' : ∀ (a : ℕ), f a < (r + 1) → a < i :=
    λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
  have hS : {a : ℕ | r < f a}ᶜ ⊆ {a : ℕ | a ≤ i} :=
    by simp only [set.compl_set_of, not_lt];
    exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
  germ.coe_lt.2 $ mem_hyperfilter_of_finite_compl $
  (set.finite_le_nat _).subset hS

theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_bot) :
  infinite_neg (of_seq f) :=
λ r, have hf' : _ := tendsto_at_top_at_bot.mp hf,
Exists.cases_on (hf' (r - 1)) $ λ i hi,
  have hi' : ∀ (a : ℕ), r - 1 < f a → a < i :=
    λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
  have hS : {a : ℕ | f a < r}ᶜ ⊆ {a : ℕ | a ≤ i} :=
    by simp only [set.compl_set_of, not_lt];
    exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
  germ.coe_lt.2 $ mem_hyperfilter_of_finite_compl $
  (set.finite_le_nat _).subset hS

lemma not_infinite_neg {x : ℝ*} : ¬ infinite x → ¬ infinite (-x) :=
not_imp_not.mpr infinite_iff_infinite_neg.mpr

lemma not_infinite_add {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
  ¬ infinite (x + y) :=
have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
Exists.cases_on hx' $ Exists.cases_on hy' $
λ r hr s hs, not_infinite_of_exists_st $ ⟨s + r, is_st_add hs hr⟩

theorem not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬ infinite x ↔ ∃ r s : ℝ, (r : ℝ*) < x ∧ x < s :=
⟨ λ hni,
Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).1) $
Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).2) $ λ r hr s hs,
by rw [not_lt] at hr hs; exact ⟨r - 1, s + 1,
  ⟨ lt_of_lt_of_le (by rw sub_eq_add_neg; norm_num) hr,
    lt_of_le_of_lt hs (by norm_num)⟩ ⟩,
λ hrs, Exists.dcases_on hrs $ λ r hr, Exists.dcases_on hr $ λ s hs,
  not_or_distrib.mpr ⟨not_forall.mpr ⟨s, lt_asymm (hs.2)⟩, not_forall.mpr ⟨r, lt_asymm (hs.1) ⟩⟩⟩

theorem not_infinite_real (r : ℝ) : ¬ infinite r := by rw not_infinite_iff_exist_lt_gt; exact
⟨ r - 1, r + 1, coe_lt_coe.2 $ sub_one_lt r, coe_lt_coe.2 $ lt_add_one r⟩

theorem not_real_of_infinite {x : ℝ*} : infinite x → ∀ r : ℝ, x ≠ r :=
λ hi r hr,  not_infinite_real r $ @eq.subst _ infinite _ _ hr hi

/-!
### Facts about `st` that require some infinite machinery
-/

private lemma is_st_mul' {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) (hs : s ≠ 0) :
  is_st (x * y) (r * s) :=
have hxr' : _ := is_st_iff_abs_sub_lt_delta.mp hxr,
have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys,
have h : _ := not_infinite_iff_exist_lt_gt.mp $ not_imp_not.mpr infinite_iff_infinite_abs.mpr $
not_infinite_of_exists_st ⟨r, hxr⟩,
Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
is_st_iff_abs_sub_lt_delta.mpr $ λ d hd,
   calc |x * y - r * s|
      = |x * (y - s) + (x - r) * s| :
        by rw [mul_sub, sub_mul, add_sub, sub_add_cancel]
  ... ≤ |x * (y - s)| + |(x - r) * s| : abs_add _ _
  ... ≤ |x| * |y - s| + |x - r| * |s| : by simp only [abs_mul]
  ... ≤ |x| * ((d / t) / 2 : ℝ) + ((d / |s|) / 2 : ℝ) * |s| : add_le_add
        (mul_le_mul_of_nonneg_left (le_of_lt $ hys' _ $ half_pos $ div_pos hd $
          coe_pos.1 $ lt_of_le_of_lt (abs_nonneg x) ht) $ abs_nonneg _)
        (mul_le_mul_of_nonneg_right (le_of_lt $ hxr' _ $ half_pos $ div_pos hd $
          abs_pos.2 hs) $ abs_nonneg _)
  ... = (d / 2 * (|x| / t) + d / 2 : ℝ*) : by
      { push_cast [-filter.germ.const_div], -- TODO: Why wasn't `hyperreal.coe_div` used?
        have : (|s| : ℝ*) ≠ 0, by simpa,
        have : (2 : ℝ*) ≠ 0 := two_ne_zero,
        field_simp [*, add_mul, mul_add, mul_assoc, mul_comm, mul_left_comm] }
  ... < (d / 2 * 1 + d / 2 : ℝ*) :
        add_lt_add_right (mul_lt_mul_of_pos_left
        ((div_lt_one $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $
        half_pos $ coe_pos.2 hd) _
  ... = (d : ℝ*) : by rw [mul_one, add_halves]

lemma is_st_mul {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
  is_st (x * y) (r * s) :=
have h : _ := not_infinite_iff_exist_lt_gt.mp $
  not_imp_not.mpr infinite_iff_infinite_abs.mpr $ not_infinite_of_exists_st ⟨r, hxr⟩,
Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
begin
  by_cases hs : s = 0,
  { apply is_st_iff_abs_sub_lt_delta.mpr, intros d hd,
    have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys (d / t)
      (div_pos hd (coe_pos.1 (lt_of_le_of_lt (abs_nonneg x) ht))),
    rw [hs, coe_zero, sub_zero] at hys',
    rw [hs, mul_zero, coe_zero, sub_zero, abs_mul, mul_comm,
        ←div_mul_cancel (d : ℝ*) (ne_of_gt (lt_of_le_of_lt (abs_nonneg x) ht)),
        ←coe_div],
    exact mul_lt_mul'' hys' ht (abs_nonneg _) (abs_nonneg _) },
  exact is_st_mul' hxr hys hs,
end

--AN INFINITE LEMMA THAT REQUIRES SOME MORE ST MACHINERY
lemma not_infinite_mul {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
  ¬ infinite (x * y) :=
have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
Exists.cases_on hx' $ Exists.cases_on hy' $ λ r hr s hs, not_infinite_of_exists_st $
⟨s * r, is_st_mul hs hr⟩
---

lemma st_add {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x + y) = st x + st y :=
have hx' : _ := is_st_st' hx,
have hy' : _ := is_st_st' hy,
have hxy : _ := is_st_st' (not_infinite_add hx hy),
have hxy' : _ := is_st_add hx' hy',
is_st_unique hxy hxy'

lemma st_neg (x : ℝ*) : st (-x) = - st x :=
if h : infinite x
then by rw [st_infinite h, st_infinite (infinite_iff_infinite_neg.mp h), neg_zero]
else is_st_unique (is_st_st' (not_infinite_neg h)) (is_st_neg (is_st_st' h))

lemma st_mul {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x * y) = (st x) * (st y) :=
have hx' : _ := is_st_st' hx,
have hy' : _ := is_st_st' hy,
have hxy : _ := is_st_st' (not_infinite_mul hx hy),
have hxy' : _ := is_st_mul hx' hy',
is_st_unique hxy hxy'

/-!
### Basic lemmas about infinitesimal
-/

theorem infinitesimal_def {x : ℝ*} :
  infinitesimal x ↔ (∀ r : ℝ, 0 < r → -(r : ℝ*) < x ∧ x < r) :=
⟨ λ hi r hr, by { convert (hi r hr); simp },
  λ hi d hd, by { convert (hi d hd); simp } ⟩

theorem lt_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, 0 < r → x < r :=
λ hi r hr, ((infinitesimal_def.mp hi) r hr).2

theorem lt_neg_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, 0 < r → -↑r < x :=
λ hi r hr, ((infinitesimal_def.mp hi) r hr).1

theorem gt_of_neg_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r < 0 → ↑r < x :=
λ hi r hr, by convert ((infinitesimal_def.mp hi) (-r) (neg_pos.mpr hr)).1;
exact (neg_neg ↑r).symm

theorem abs_lt_real_iff_infinitesimal {x : ℝ*} :
  infinitesimal x ↔ ∀ r : ℝ, r ≠ 0 → |x| < |r| :=
⟨ λ hi r hr, abs_lt.mpr (by rw ←coe_abs;
  exact infinitesimal_def.mp hi (|r|) (abs_pos.2 hr)),
  λ hR, infinitesimal_def.mpr $ λ r hr, abs_lt.mp $
  (abs_of_pos $ coe_pos.2 hr) ▸ hR r $ ne_of_gt hr ⟩

lemma infinitesimal_zero : infinitesimal 0 := is_st_refl_real 0

lemma zero_of_infinitesimal_real {r : ℝ} : infinitesimal r → r = 0 := eq_of_is_st_real

lemma zero_iff_infinitesimal_real {r : ℝ} : infinitesimal r ↔ r = 0 :=
⟨zero_of_infinitesimal_real, λ hr, by rw hr; exact infinitesimal_zero⟩

lemma infinitesimal_add {x y : ℝ*} (hx : infinitesimal x) (hy : infinitesimal y) :
  infinitesimal (x + y) :=
by simpa only [add_zero] using is_st_add hx hy

lemma infinitesimal_neg {x : ℝ*} (hx : infinitesimal x) : infinitesimal (-x) :=
by simpa only [neg_zero] using is_st_neg hx

lemma infinitesimal_neg_iff {x : ℝ*} : infinitesimal x ↔ infinitesimal (-x) :=
⟨infinitesimal_neg, λ h, (neg_neg x) ▸ @infinitesimal_neg (-x) h⟩

lemma infinitesimal_mul {x y : ℝ*} (hx : infinitesimal x) (hy : infinitesimal y) :
  infinitesimal (x * y) :=
by simpa only [mul_zero] using is_st_mul hx hy

theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} :
  tendsto f at_top (𝓝 0) → infinitesimal (of_seq f) :=
λ hf d hd, by rw [sub_eq_add_neg, ←coe_neg, ←coe_add, ←coe_add, zero_add, zero_add];
exact ⟨neg_lt_of_tendsto_zero_of_pos hf hd, lt_of_tendsto_zero_of_pos hf hd⟩

theorem infinitesimal_epsilon : infinitesimal ε :=
infinitesimal_of_tendsto_zero tendsto_inverse_at_top_nhds_0_nat

lemma not_real_of_infinitesimal_ne_zero (x : ℝ*) :
  infinitesimal x → x ≠ 0 → ∀ r : ℝ, x ≠ r :=
λ hi hx r hr, hx $ hr.trans $ coe_eq_zero.2 $
is_st_unique (hr.symm ▸ is_st_refl_real r : is_st x r) hi

theorem infinitesimal_sub_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : infinitesimal (x - r) :=
show is_st (x - r) 0,
by { rw [sub_eq_add_neg, ← add_neg_self r], exact is_st_add hxr (is_st_refl_real (-r)) }

theorem infinitesimal_sub_st {x : ℝ*} (hx : ¬infinite x) : infinitesimal (x - st x) :=
infinitesimal_sub_is_st $ is_st_st' hx

lemma infinite_pos_iff_infinitesimal_inv_pos {x : ℝ*} :
  infinite_pos x ↔ (infinitesimal x⁻¹ ∧ 0 < x⁻¹) :=
⟨ λ hip, ⟨ infinitesimal_def.mpr $ λ r hr,
  ⟨ lt_trans (coe_lt_coe.2 (neg_neg_of_pos hr)) (inv_pos.2 (hip 0)),
    (inv_lt (coe_lt_coe.2 hr) (hip 0)).mp (by convert hip r⁻¹) ⟩,
  inv_pos.2 $ hip 0 ⟩,
  λ ⟨hi, hp⟩ r, @classical.by_cases (r = 0) (↑r < x) (λ h, eq.substr h (inv_pos.mp hp)) $
  λ h, lt_of_le_of_lt (coe_le_coe.2 (le_abs_self r))
  ((inv_lt_inv (inv_pos.mp hp) (coe_lt_coe.2 (abs_pos.2 h))).mp
  ((infinitesimal_def.mp hi) ((|r|)⁻¹) (inv_pos.2 (abs_pos.2 h))).2) ⟩

lemma infinite_neg_iff_infinitesimal_inv_neg {x : ℝ*} :
  infinite_neg x ↔ (infinitesimal x⁻¹ ∧ x⁻¹ < 0) :=
⟨ λ hin, have hin' : _ := infinite_pos_iff_infinitesimal_inv_pos.mp
  (infinite_pos_neg_of_infinite_neg hin),
  by rwa [infinitesimal_neg_iff, ←neg_pos, neg_inv],
  λ hin, by rwa [←neg_pos, infinitesimal_neg_iff, neg_inv,
    ←infinite_pos_iff_infinitesimal_inv_pos, ←infinite_neg_iff_infinite_pos_neg] at hin ⟩

theorem infinitesimal_inv_of_infinite {x : ℝ*} : infinite x → infinitesimal x⁻¹ :=
λ hi, or.cases_on hi
 (λ hip, (infinite_pos_iff_infinitesimal_inv_pos.mp hip).1)
 (λ hin, (infinite_neg_iff_infinitesimal_inv_neg.mp hin).1)

theorem infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : infinitesimal x⁻¹ ) :
  infinite x :=
begin
  cases (lt_or_gt_of_ne h0) with hn hp,
  { exact or.inr (infinite_neg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩) },
  { exact or.inl (infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩) }
end

theorem infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) : infinite x ↔ infinitesimal x⁻¹ :=
⟨ infinitesimal_inv_of_infinite, infinite_of_infinitesimal_inv h0 ⟩

lemma infinitesimal_pos_iff_infinite_pos_inv {x : ℝ*} :
  infinite_pos x⁻¹ ↔ (infinitesimal x ∧ 0 < x) :=
by convert infinite_pos_iff_infinitesimal_inv_pos; simp only [inv_inv₀]

lemma infinitesimal_neg_iff_infinite_neg_inv {x : ℝ*} :
  infinite_neg x⁻¹ ↔ (infinitesimal x ∧ x < 0) :=
by convert infinite_neg_iff_infinitesimal_inv_neg; simp only [inv_inv₀]

theorem infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : infinitesimal x ↔ infinite x⁻¹ :=
by convert (infinite_iff_infinitesimal_inv (inv_ne_zero h)).symm; simp only [inv_inv₀]

/-!
### `st` stuff that requires infinitesimal machinery
-/

theorem is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : tendsto f at_top (𝓝 r)) :
  is_st (of_seq f) r :=
have hg : tendsto (λ n, f n - r) at_top (𝓝 0) :=
  (sub_self r) ▸ (hf.sub tendsto_const_nhds),
by rw [←(zero_add r), ←(sub_add_cancel f (λ n, r))];
exact is_st_add (infinitesimal_of_tendsto_zero hg) (is_st_refl_real r)

lemma is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬ infinitesimal x) : is_st x r → is_st x⁻¹ r⁻¹ :=
λ hxr, have h : x ≠ 0 := (λ h, hi (h.symm ▸ infinitesimal_zero)),
have H : _ := exists_st_of_not_infinite $ not_imp_not.mpr (infinitesimal_iff_infinite_inv h).mpr hi,
Exists.cases_on H $ λ s hs,
have H' : is_st 1 (r * s) := mul_inv_cancel h ▸ is_st_mul hxr hs,
have H'' : s = r⁻¹ := one_div r ▸ eq_one_div_of_mul_eq_one (eq_of_is_st_real H').symm,
H'' ▸ hs

lemma st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ :=
begin
  by_cases h0 : x = 0,
  rw [h0, inv_zero, ←coe_zero, st_id_real, inv_zero],
  by_cases h1 : infinitesimal x,
  rw [st_infinite ((infinitesimal_iff_infinite_inv h0).mp h1), st_of_is_st h1, inv_zero],
  by_cases h2 : infinite x,
  rw [st_of_is_st (infinitesimal_inv_of_infinite h2), st_infinite h2, inv_zero],
  exact st_of_is_st (is_st_inv h1 (is_st_st' h2)),
end

/-!
### Infinite stuff that requires infinitesimal machinery
-/

lemma infinite_pos_omega : infinite_pos ω :=
infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨infinitesimal_epsilon, epsilon_pos⟩

lemma infinite_omega : infinite ω :=
(infinite_iff_infinitesimal_inv omega_ne_zero).mpr infinitesimal_epsilon

lemma infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos {x y : ℝ*} :
  infinite_pos x → ¬ infinitesimal y → 0 < y → infinite_pos (x * y) :=
λ hx hy₁ hy₂ r, have hy₁' : _ := not_forall.mp (by rw infinitesimal_def at hy₁; exact hy₁),
Exists.dcases_on hy₁' $ λ r₁ hy₁'',
have hyr : _ := by rw [not_imp, ←abs_lt, not_lt, abs_of_pos hy₂] at hy₁''; exact hy₁'',
by rw [←div_mul_cancel r (ne_of_gt hyr.1), coe_mul];
exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))

lemma infinite_pos_mul_of_not_infinitesimal_pos_infinite_pos {x y : ℝ*} :
  ¬ infinitesimal x → 0 < x → infinite_pos y → infinite_pos (x * y) :=
λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos hy hx hp

lemma infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg {x y : ℝ*} :
  infinite_neg x → ¬ infinitesimal y → y < 0 → infinite_pos (x * y) :=
by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, ←neg_mul_neg, infinitesimal_neg_iff];
exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos

lemma infinite_pos_mul_of_not_infinitesimal_neg_infinite_neg {x y : ℝ*} :
  ¬ infinitesimal x → x < 0 → infinite_neg y → infinite_pos (x * y) :=
λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg hy hx hp

lemma infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg {x y : ℝ*} :
  infinite_pos x → ¬ infinitesimal y → y < 0 → infinite_neg (x * y) :=
by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, neg_mul_eq_mul_neg, infinitesimal_neg_iff];
exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos

lemma infinite_neg_mul_of_not_infinitesimal_neg_infinite_pos {x y : ℝ*} :
  ¬ infinitesimal x → x < 0 → infinite_pos y → infinite_neg (x * y) :=
λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg hy hx hp

lemma infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos {x y : ℝ*} :
  infinite_neg x → ¬ infinitesimal y → 0 < y → infinite_neg (x * y) :=
by rw [infinite_neg_iff_infinite_pos_neg, infinite_neg_iff_infinite_pos_neg, neg_mul_eq_neg_mul];
exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos

lemma infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg {x y : ℝ*} :
  ¬ infinitesimal x → 0 < x → infinite_neg y → infinite_neg (x * y) :=
λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos hy hx hp

lemma infinite_pos_mul_infinite_pos {x y : ℝ*} :
  infinite_pos x → infinite_pos y → infinite_pos (x * y) :=
λ hx hy, infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
hx (not_infinitesimal_of_infinite_pos hy) (hy 0)

lemma infinite_neg_mul_infinite_neg {x y : ℝ*} :
  infinite_neg x → infinite_neg y → infinite_pos (x * y) :=
λ hx hy, infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg
hx (not_infinitesimal_of_infinite_neg hy) (hy 0)

lemma infinite_pos_mul_infinite_neg {x y : ℝ*} :
  infinite_pos x → infinite_neg y → infinite_neg (x * y) :=
λ hx hy, infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg
hx (not_infinitesimal_of_infinite_neg hy) (hy 0)

lemma infinite_neg_mul_infinite_pos {x y : ℝ*} :
  infinite_neg x → infinite_pos y → infinite_neg (x * y) :=
λ hx hy, infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos
hx (not_infinitesimal_of_infinite_pos hy) (hy 0)

lemma infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} :
  infinite x → ¬ infinitesimal y → infinite (x * y) :=
λ hx hy, have h0 : y < 0 ∨ 0 < y := lt_or_gt_of_ne (λ H0, hy (eq.substr H0 (is_st_refl_real 0))),
or.dcases_on hx
  (or.dcases_on h0
    (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg Hx hy H0))
    (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos Hx hy H0)))
  (or.dcases_on h0
    (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg Hx hy H0))
    (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos Hx hy H0)))

lemma infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} :
  ¬ infinitesimal x → infinite y → infinite (x * y) :=
λ hx hy, by rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx

lemma infinite_mul_infinite {x y : ℝ*} : infinite x → infinite y → infinite (x * y) :=
λ hx hy, infinite_mul_of_infinite_not_infinitesimal hx (not_infinitesimal_of_infinite hy)

end hyperreal

author: jjaassoonn


import utils

/-- A structure for storing mathematical statements together with docstrings and other relevant information. -/
structure declaration_with_docstring :=
  (is_definition : bool)
  (decl_name : string)
  (args : string)
  (type : string)
  (doc_string : string)

namespace declaration_with_docstring

/-- Retrieves a declaration from the environment by its name. -/
meta def from_name (n : name) : tactic declaration_with_docstring := do
  env ← tactic.get_env,
  decl ← env.get n,
  t ← tactic.pp decl.type,
  let stmt := to_string t,
  doc_str ← tactic.doc_string n,
  return {
    is_definition := decl.is_definition,
    decl_name := to_string n,
    args := "",
    type := stmt,
    doc_string := doc_str,
  }

/-- Retrieves all declarations with docstrings in the current module. -/
meta def module_decls : tactic (list declaration_with_docstring) := do
  mod_docs ← tactic.module_doc_strings,
  -- keep only docstrings corresponding to declarations
  let mod_docs' := mod_docs.filter_map prod.fst,
  mod_docs'.mmap from_name

/-- Checks whether a declaration is type-correct. -/
meta def validate : declaration_with_docstring → tactic (option unit)
  | ⟨_, _, args, type, _⟩ := tactic.try_core $
      let full_type := if args.is_empty then type else
                          sformat!"Π {args}, {type}" in
        parse_str full_type >>= λ _, pure ()

/-- Convert a declaration to a `json` object. -/
meta def to_json : declaration_with_docstring → json
  | ⟨_, nm, args, type, _⟩ :=
    json.object $ [
      ("name", nm),
      ("args", args),
      ("type", type)
    ]

/-- Convert a declaration to a `json` object, including information such as the docstring. -/
meta def to_full_json : declaration_with_docstring → json
  | ⟨is_def, nm, args, type, doc_str⟩ :=
    json.object $ [
      ("is_def", json.of_bool is_def),
      ("name", nm),
      ("args", args),
      ("type", type),
      ("doc_string", doc_str)
    ]

/-- Displays a declaration as a string. -/
def to_string : declaration_with_docstring → string
  | ⟨is_def, nm, args, type, _⟩ :=
    let header :=
      (match is_def with
        | ff := "theorem"
        | tt := "def"
      end) in
    sformat!"{header} {nm}{args}:{type}"

/-- Displays a declaration and its docstring as a string. -/
def to_full_string : declaration_with_docstring → string
  | d := sformat!"/-- {d.doc_string} -/ \n {d.to_string}"

/-- The json input is assumed to be an object with all the relevant fields. -/
meta def from_json (j : json) : except string declaration_with_docstring := do
  decl_name ← j.lookup_as "name" json.as_string,
  args ← j.lookup_as "args" json.as_string,
  type ← j.lookup_as "type" json.as_string,
  doc_string ← j.lookup_as "doc_string" json.as_string,
  -- TODO: Extract `is_definition` once `defdocs` is merged
  return ⟨ff, decl_name, args, type, doc_string⟩

/-- Parses a string of the form "<theorem/def> <name> <(arg₁) (arg₂) … (argₙ)> : <type>"
    as a `declaration_with_docstring`. -/
def from_string (decl : string) (doc_str := "") : declaration_with_docstring :=
  let decl := decl.drop_while $ λ c, c.is_whitespace in
  let (decl_head, named_term) := decl.take_until $ λ c, (c.is_whitespace ∨ c = ',' ∨ c = ':' ∨ c = ';' ∨ c = '-') in
  let named_term := named_term.drop_while $ λ c, c.is_whitespace in
  let (decl_name, args_with_type) := named_term.take_until $ λ c, (c.is_whitespace ∨ c = ',' ∨ c = ':' ∨ c = ';' ∨ c = '-' ∨ c.is_left_bracket) in
  let (args, type) := process_args args_with_type in
  { is_definition := decl_head = "def",
    decl_name := decl_name,
    args := args.drop_while $ λ c, c.is_whitespace,
    type := type,
    doc_string := doc_str }

-- #eval declaration_with_docstring.args (from_string "theorem abc (n : ℕ) : n = n")

end declaration_with_docstring


text:
import LMT

variable {I} [Nonempty I] {E} [Nonempty E] [Nonempty (A I E)]

example {a1 a2 a3 : A I E} :
        ((a1).read i3) ≠ (((a1).write i1 ((a1).read i3)).read i3) → False := by
  arr

repo: ar-project


text:
/-
Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro

! This file was ported from Lean 3 source module data.nat.pow
! leanprover-community/mathlib commit 55d224c38461be1e8e4363247dd110137c24a4ff
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Algebra.GroupPower.Order

/-! # `nat.pow`

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

Results on the power operation on natural numbers.
-/

namespace Nat

/-! ### `pow` -/

#print Nat.pow_le_pow_of_le_left /-
-- This is redundant with `pow_le_pow_of_le_left'`,
-- We leave a version in the `nat` namespace as well.
-- (The global `pow_le_pow_of_le_left` needs an extra hypothesis `0 ≤ x`.)
protected theorem pow_le_pow_of_le_left {x y : ℕ} (H : x ≤ y) : ∀ i : ℕ, x ^ i ≤ y ^ i :=
  pow_le_pow_of_le_left' H
#align nat.pow_le_pow_of_le_left Nat.pow_le_pow_of_le_left
-/

#print Nat.pow_le_pow_of_le_right /-
theorem pow_le_pow_of_le_right {x : ℕ} (H : 0 < x) {i j : ℕ} (h : i ≤ j) : x ^ i ≤ x ^ j :=
  pow_le_pow' H h
#align nat.pow_le_pow_of_le_right Nat.pow_le_pow_of_le_right
-/

#print Nat.pow_lt_pow_of_lt_left /-
theorem pow_lt_pow_of_lt_left {x y : ℕ} (H : x < y) {i} (h : 0 < i) : x ^ i < y ^ i :=
  pow_lt_pow_of_lt_left H (zero_le _) h
#align nat.pow_lt_pow_of_lt_left Nat.pow_lt_pow_of_lt_left
-/

#print Nat.pow_lt_pow_of_lt_right /-
theorem pow_lt_pow_of_lt_right {x : ℕ} (H : 1 < x) {i j : ℕ} (h : i < j) : x ^ i < x ^ j :=
  pow_lt_pow H h
#align nat.pow_lt_pow_of_lt_right Nat.pow_lt_pow_of_lt_right
-/

#print Nat.pow_lt_pow_succ /-
theorem pow_lt_pow_succ {p : ℕ} (h : 1 < p) (n : ℕ) : p ^ n < p ^ (n + 1) :=
  pow_lt_pow_of_lt_right h n.lt_succ_self
#align nat.pow_lt_pow_succ Nat.pow_lt_pow_succ
-/

#print Nat.le_self_pow /-
theorem le_self_pow {n : ℕ} (hn : n ≠ 0) : ∀ m : ℕ, m ≤ m ^ n
  | 0 => zero_le _
  | m + 1 => le_self_pow (by decide) hn
#align nat.le_self_pow Nat.le_self_pow
-/

#print Nat.lt_pow_self /-
theorem lt_pow_self {p : ℕ} (h : 1 < p) : ∀ n : ℕ, n < p ^ n
  | 0 => by simp [zero_lt_one]
  | n + 1 =>
    calc
      n + 1 < p ^ n + 1 := Nat.add_lt_add_right (lt_pow_self _) _
      _ ≤ p ^ (n + 1) := pow_lt_pow_succ h _

#align nat.lt_pow_self Nat.lt_pow_self
-/

#print Nat.lt_two_pow /-
theorem lt_two_pow (n : ℕ) : n < 2 ^ n :=
  lt_pow_self (by decide) n
#align nat.lt_two_pow Nat.lt_two_pow
-/

#print Nat.one_le_pow /-
theorem one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n :=
  by
  rw [← one_pow n]
  exact Nat.pow_le_pow_of_le_left h n
#align nat.one_le_pow Nat.one_le_pow
-/

#print Nat.one_le_pow' /-
theorem one_le_pow' (n m : ℕ) : 1 ≤ (m + 1) ^ n :=
  one_le_pow n (m + 1) (succ_pos m)
#align nat.one_le_pow' Nat.one_le_pow'
-/

#print Nat.one_le_two_pow /-
theorem one_le_two_pow (n : ℕ) : 1 ≤ 2 ^ n :=
  one_le_pow n 2 (by decide)
#align nat.one_le_two_pow Nat.one_le_two_pow
-/

#print Nat.one_lt_pow /-
theorem one_lt_pow (n m : ℕ) (h₀ : 0 < n) (h₁ : 1 < m) : 1 < m ^ n :=
  by
  rw [← one_pow n]
  exact pow_lt_pow_of_lt_left h₁ h₀
#align nat.one_lt_pow Nat.one_lt_pow
-/

#print Nat.one_lt_pow' /-
theorem one_lt_pow' (n m : ℕ) : 1 < (m + 2) ^ (n + 1) :=
  one_lt_pow (n + 1) (m + 2) (succ_pos n) (Nat.lt_of_sub_eq_succ rfl)
#align nat.one_lt_pow' Nat.one_lt_pow'
-/

#print Nat.one_lt_pow_iff /-
@[simp]
theorem one_lt_pow_iff {k n : ℕ} (h : 0 ≠ k) : 1 < n ^ k ↔ 1 < n :=
  by
  cases n
  · cases k <;> simp [zero_pow_eq]
  cases n
  · rw [one_pow]
  refine' ⟨fun _ => one_lt_succ_succ n, fun _ => _⟩
  induction' k with k hk
  · exact absurd rfl h
  cases k
  · simp
  exact one_lt_mul (one_lt_succ_succ _).le (hk (succ_ne_zero k).symm)
#align nat.one_lt_pow_iff Nat.one_lt_pow_iff
-/

#print Nat.one_lt_two_pow /-
theorem one_lt_two_pow (n : ℕ) (h₀ : 0 < n) : 1 < 2 ^ n :=
  one_lt_pow n 2 h₀ (by decide)
#align nat.one_lt_two_pow Nat.one_lt_two_pow
-/

#print Nat.one_lt_two_pow' /-
theorem one_lt_two_pow' (n : ℕ) : 1 < 2 ^ (n + 1) :=
  one_lt_pow (n + 1) 2 (succ_pos n) (by decide)
#align nat.one_lt_two_pow' Nat.one_lt_two_pow'
-/

#print Nat.pow_right_strictMono /-
theorem pow_right_strictMono {x : ℕ} (k : 2 ≤ x) : StrictMono fun n : ℕ => x ^ n := fun _ _ =>
  pow_lt_pow_of_lt_right k
#align nat.pow_right_strict_mono Nat.pow_right_strictMono
-/

#print Nat.pow_le_iff_le_right /-
theorem pow_le_iff_le_right {x m n : ℕ} (k : 2 ≤ x) : x ^ m ≤ x ^ n ↔ m ≤ n :=
  StrictMono.le_iff_le (pow_right_strictMono k)
#align nat.pow_le_iff_le_right Nat.pow_le_iff_le_right
-/

#print Nat.pow_lt_iff_lt_right /-
theorem pow_lt_iff_lt_right {x m n : ℕ} (k : 2 ≤ x) : x ^ m < x ^ n ↔ m < n :=
  StrictMono.lt_iff_lt (pow_right_strictMono k)
#align nat.pow_lt_iff_lt_right Nat.pow_lt_iff_lt_right
-/

#print Nat.pow_right_injective /-
theorem pow_right_injective {x : ℕ} (k : 2 ≤ x) : Function.Injective fun n : ℕ => x ^ n :=
  StrictMono.injective (pow_right_strictMono k)
#align nat.pow_right_injective Nat.pow_right_injective
-/

#print Nat.pow_left_strictMono /-
theorem pow_left_strictMono {m : ℕ} (k : 1 ≤ m) : StrictMono fun x : ℕ => x ^ m := fun _ _ h =>
  pow_lt_pow_of_lt_left h k
#align nat.pow_left_strict_mono Nat.pow_left_strictMono
-/

#print Nat.mul_lt_mul_pow_succ /-
theorem mul_lt_mul_pow_succ {n a q : ℕ} (a0 : 0 < a) (q1 : 1 < q) : n * q < a * q ^ (n + 1) :=
  by
  rw [pow_succ', ← mul_assoc, mul_lt_mul_right (zero_lt_one.trans q1)]
  exact lt_mul_of_one_le_of_lt (nat.succ_le_iff.mpr a0) (Nat.lt_pow_self q1 n)
#align nat.mul_lt_mul_pow_succ Nat.mul_lt_mul_pow_succ
-/

end Nat

#print StrictMono.nat_pow /-
theorem StrictMono.nat_pow {n : ℕ} (hn : 1 ≤ n) {f : ℕ → ℕ} (hf : StrictMono f) :
    StrictMono fun m => f m ^ n :=
  (Nat.pow_left_strictMono hn).comp hf
#align strict_mono.nat_pow StrictMono.nat_pow
-/

namespace Nat

#print Nat.pow_le_iff_le_left /-
theorem pow_le_iff_le_left {m x y : ℕ} (k : 1 ≤ m) : x ^ m ≤ y ^ m ↔ x ≤ y :=
  StrictMono.le_iff_le (pow_left_strictMono k)
#align nat.pow_le_iff_le_left Nat.pow_le_iff_le_left
-/

#print Nat.pow_lt_iff_lt_left /-
theorem pow_lt_iff_lt_left {m x y : ℕ} (k : 1 ≤ m) : x ^ m < y ^ m ↔ x < y :=
  StrictMono.lt_iff_lt (pow_left_strictMono k)
#align nat.pow_lt_iff_lt_left Nat.pow_lt_iff_lt_left
-/

#print Nat.pow_left_injective /-
theorem pow_left_injective {m : ℕ} (k : 1 ≤ m) : Function.Injective fun x : ℕ => x ^ m :=
  StrictMono.injective (pow_left_strictMono k)
#align nat.pow_left_injective Nat.pow_left_injective
-/

#print Nat.sq_sub_sq /-
theorem sq_sub_sq (a b : ℕ) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
  by
  rw [sq, sq]
  exact Nat.mul_self_sub_mul_self_eq a b
#align nat.sq_sub_sq Nat.sq_sub_sq
-/

alias sq_sub_sq ← pow_two_sub_pow_two
#align nat.pow_two_sub_pow_two Nat.pow_two_sub_pow_two

/-! ### `pow` and `mod` / `dvd` -/

#print Nat.pow_mod /-
theorem pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n :=
  by
  induction' b with b ih
  rfl; simp [pow_succ, Nat.mul_mod, ih]
#align nat.pow_mod Nat.pow_mod
-/

#print Nat.mod_pow_succ /-
theorem mod_pow_succ {b : ℕ} (w m : ℕ) : m % b ^ succ w = b * (m / b % b ^ w) + m % b :=
  by
  by_cases b_h : b = 0
  · simp [b_h, pow_succ]
  have b_pos := Nat.pos_of_ne_zero b_h
  apply Nat.strong_induction_on m
  clear m
  intro p IH
  cases' lt_or_ge p (b ^ succ w) with h₁ h₁
  -- base case: p < b^succ w
  · have h₂ : p / b < b ^ w := by
      rw [div_lt_iff_lt_mul b_pos]
      simpa [pow_succ'] using h₁
    rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂]
    simp [div_add_mod]
  -- step: p ≥ b^succ w
  · -- Generate condition for induction hypothesis
    have h₂ : p - b ^ succ w < p := tsub_lt_self ((pow_pos b_pos _).trans_le h₁) (pow_pos b_pos _)
    -- Apply induction
    rw [mod_eq_sub_mod h₁, IH _ h₂]
    -- Normalize goal and h1
    simp only [pow_succ]
    simp only [GE.ge, pow_succ] at h₁
    -- Pull subtraction outside mod and div
    rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁]
    -- Cancel subtraction inside mod b^w
    have p_b_ge : b ^ w ≤ p / b :=
      by
      rw [le_div_iff_mul_le b_pos, mul_comm]
      exact h₁
    rw [Eq.symm (mod_eq_sub_mod p_b_ge)]
#align nat.mod_pow_succ Nat.mod_pow_succ
-/

#print Nat.pow_dvd_pow_iff_pow_le_pow /-
theorem pow_dvd_pow_iff_pow_le_pow {k l : ℕ} : ∀ {x : ℕ} (w : 0 < x), x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l
  | x + 1, w => by
    constructor
    · intro a
      exact le_of_dvd (pow_pos (succ_pos x) l) a
    · intro a
      cases' x with x
      · simp only [one_pow]
      · have le := (pow_le_iff_le_right (Nat.le_add_left _ _)).mp a
        use (x + 2) ^ (l - k)
        rw [← pow_add, add_comm k, tsub_add_cancel_of_le le]
#align nat.pow_dvd_pow_iff_pow_le_pow Nat.pow_dvd_pow_iff_pow_le_pow
-/

#print Nat.pow_dvd_pow_iff_le_right /-
/-- If `1 < x`, then `x^k` divides `x^l` if and only if `k` is at most `l`. -/
theorem pow_dvd_pow_iff_le_right {x k l : ℕ} (w : 1 < x) : x ^ k ∣ x ^ l ↔ k ≤ l := by
  rw [pow_dvd_pow_iff_pow_le_pow (lt_of_succ_lt w), pow_le_iff_le_right w]
#align nat.pow_dvd_pow_iff_le_right Nat.pow_dvd_pow_iff_le_right
-/

#print Nat.pow_dvd_pow_iff_le_right' /-
theorem pow_dvd_pow_iff_le_right' {b k l : ℕ} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l :=
  pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl)
#align nat.pow_dvd_pow_iff_le_right' Nat.pow_dvd_pow_iff_le_right'
-/

#print Nat.not_pos_pow_dvd /-
theorem not_pos_pow_dvd : ∀ {p k : ℕ} (hp : 1 < p) (hk : 1 < k), ¬p ^ k ∣ p
  | succ p, succ k, hp, hk, h =>
    have : succ p * succ p ^ k ∣ succ p * 1 := by simpa [pow_succ] using h
    have : succ p ^ k ∣ 1 := dvd_of_mul_dvd_mul_left (succ_pos _) this
    have he : succ p ^ k = 1 := eq_one_of_dvd_one this
    have : k < succ p ^ k := lt_pow_self hp k
    have : k < 1 := by rwa [he] at this
    have : k = 0 := Nat.eq_zero_of_le_zero <| le_of_lt_succ this
    have : 1 < 1 := by rwa [this] at hk
    absurd this (by decide)
#align nat.not_pos_pow_dvd Nat.not_pos_pow_dvd
-/

#print Nat.pow_dvd_of_le_of_pow_dvd /-
theorem pow_dvd_of_le_of_pow_dvd {p m n k : ℕ} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) : p ^ m ∣ k :=
  (pow_dvd_pow _ hmn).trans hdiv
#align nat.pow_dvd_of_le_of_pow_dvd Nat.pow_dvd_of_le_of_pow_dvd
-/

#print Nat.dvd_of_pow_dvd /-
theorem dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m := by
  rw [← pow_one p] <;> exact pow_dvd_of_le_of_pow_dvd hk hpk
#align nat.dvd_of_pow_dvd Nat.dvd_of_pow_dvd
-/

#print Nat.pow_div /-
theorem pow_div {x m n : ℕ} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n) := by
  rw [Nat.div_eq_iff_eq_mul_left (pow_pos hx n) (pow_dvd_pow _ h), pow_sub_mul_pow _ h]
#align nat.pow_div Nat.pow_div
-/

#print Nat.lt_of_pow_dvd_right /-
theorem lt_of_pow_dvd_right {p i n : ℕ} (hn : n ≠ 0) (hp : 2 ≤ p) (h : p ^ i ∣ n) : i < n :=
  by
  rw [← pow_lt_iff_lt_right hp]
  exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n)
#align nat.lt_of_pow_dvd_right Nat.lt_of_pow_dvd_right
-/

end Nat

author: leanprover-community