[GOAL]
⊢ Tendsto (fun k => ∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 (π / 4))
[PROOFSTEP]
rw [tendsto_iff_norm_tendsto_zero, ← tendsto_zero_iff_norm_tendsto_zero]
  -- (1) We introduce a useful sequence `u` of values in [0,1], then prove that another sequence
    --     constructed from `u` tends to `0` at `+∞`
[GOAL]
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
let u := fun k : ℕ => (k : NNReal) ^ (-1 / (2 * (k : ℝ) + 1))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
have H : Tendsto (fun k : ℕ => (1 : ℝ) - u k + u k ^ (2 * (k : ℝ) + 1)) atTop (𝓝 0) :=
  by
  convert
    (((tendsto_rpow_div_mul_add (-1) 2 1 two_ne_zero.symm).neg.const_add 1).add tendsto_inv_atTop_zero).comp
      tendsto_nat_cast_atTop_atTop using
    1
  · ext k
    simp only [NNReal.coe_nat_cast, Function.comp_apply, NNReal.coe_rpow]
    rw [← rpow_mul (Nat.cast_nonneg k) (-1 / (2 * (k : ℝ) + 1)) (2 * (k : ℝ) + 1),
      @div_mul_cancel _ _ (2 * (k : ℝ) + 1) _ (by norm_cast; simp only [Nat.succ_ne_zero, not_false_iff]),
      rpow_neg_one k, sub_eq_add_neg]
  ·
    simp only [add_zero, add_right_neg]
      -- (2) We convert the limit in our goal to an inequality
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
[PROOFSTEP]
convert
  (((tendsto_rpow_div_mul_add (-1) 2 1 two_ne_zero.symm).neg.const_add 1).add tendsto_inv_atTop_zero).comp
    tendsto_nat_cast_atTop_atTop using
  1
[GOAL]
case h.e'_3
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) = (fun x => 1 + -x ^ (-1 / (2 * x + 1)) + x⁻¹) ∘ Nat.cast
[PROOFSTEP]
ext k
[GOAL]
case h.e'_3.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1)) = ((fun x => 1 + -x ^ (-1 / (2 * x + 1)) + x⁻¹) ∘ Nat.cast) k
[PROOFSTEP]
simp only [NNReal.coe_nat_cast, Function.comp_apply, NNReal.coe_rpow]
[GOAL]
case h.e'_3.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 1 - ↑k ^ (-1 / (2 * ↑k + 1)) + (↑k ^ (-1 / (2 * ↑k + 1))) ^ (2 * ↑k + 1) = 1 + -↑k ^ (-1 / (2 * ↑k + 1)) + (↑k)⁻¹
[PROOFSTEP]
rw [← rpow_mul (Nat.cast_nonneg k) (-1 / (2 * (k : ℝ) + 1)) (2 * (k : ℝ) + 1),
  @div_mul_cancel _ _ (2 * (k : ℝ) + 1) _ (by norm_cast; simp only [Nat.succ_ne_zero, not_false_iff]), rpow_neg_one k,
  sub_eq_add_neg]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ 2 * ↑k + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
⊢ ¬2 * k + 1 = 0
[PROOFSTEP]
simp only [Nat.succ_ne_zero, not_false_iff]
[GOAL]
case h.e'_5
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
⊢ 𝓝 0 = 𝓝 (1 + -1 + 0)
[PROOFSTEP]
simp only [add_zero, add_right_neg]
  -- (2) We convert the limit in our goal to an inequality
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
⊢ Tendsto (fun e => ∑ i in Finset.range e, (-1) ^ i / (2 * ↑i + 1) - π / 4) atTop (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero_norm _ H
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
⊢ ∀ (n : ℕ), ‖∑ i in Finset.range n, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u n) + ↑(u n ^ (2 * ↑n + 1))
[PROOFSTEP]
intro k
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let U := u k
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let b (i : ℕ) x := (-(1 : ℝ)) ^ i * x ^ (2 * i + 1) / (2 * i + 1)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
let f x := arctan x - ∑ i in Finset.range k, b i x
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
suffices f_bound : |f 1 - f 0| ≤ (1 : ℝ) - U + U ^ (2 * (k : ℝ) + 1)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
rw [← norm_neg]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖-(∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4)‖ ≤ 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
convert f_bound using 1
[GOAL]
case h.e'_3
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f_bound : |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
⊢ ‖-(∑ i in Finset.range k, (-1) ^ i / (2 * ↑i + 1) - π / 4)‖ = |f 1 - f 0|
[PROOFSTEP]
simp
  -- We show that `U` is indeed in [0,1]
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hU1 : (U : ℝ) ≤ 1 := by
  by_cases hk : k = 0
  · simp [hk]
  ·
    exact
      rpow_le_one_of_one_le_of_nonpos (by norm_cast; exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk))
        (le_of_lt
          (@div_neg_of_neg_of_pos _ _ (-(1 : ℝ)) (2 * k + 1) (neg_neg_iff_pos.mpr zero_lt_one)
            (by norm_cast; exact Nat.succ_pos')))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
⊢ ↑U ≤ 1
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : k = 0
⊢ ↑U ≤ 1
[PROOFSTEP]
simp [hk]
[GOAL]
case neg
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ ↑U ≤ 1
[PROOFSTEP]
exact
  rpow_le_one_of_one_le_of_nonpos (by norm_cast; exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk))
    (le_of_lt
      (@div_neg_of_neg_of_pos _ _ (-(1 : ℝ)) (2 * k + 1) (neg_neg_iff_pos.mpr zero_lt_one)
        (by norm_cast; exact Nat.succ_pos')))
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 1 ≤ ↑↑k
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 1 ≤ k
[PROOFSTEP]
exact Nat.succ_le_iff.mpr (Nat.pos_of_ne_zero hk)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 0 < 2 * ↑k + 1
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hk : ¬k = 0
⊢ 0 < 2 * k + 1
[PROOFSTEP]
exact Nat.succ_pos'
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hU2 := NNReal.coe_nonneg U
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
let f' := fun x : ℝ => (-x ^ 2) ^ k / (1 + x ^ 2)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have has_deriv_at_f : ∀ x, HasDerivAt f (f' x) x := by
  intro x
  have has_deriv_at_b : ∀ i ∈ Finset.range k, HasDerivAt (b i) ((-x ^ 2) ^ i) x :=
    by
    intro i _
    convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
    · ext y
      simp only [id.def]
      ring
    · simp
      rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
        mul_pow (-1 : ℝ) (x ^ 2) i]
      ring_nf
  convert (hasDerivAt_arctan x).sub (HasDerivAt.sum has_deriv_at_b) using 1
  have g_sum := @geom_sum_eq _ _ (-x ^ 2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k
  simp only at g_sum ⊢
  rw [g_sum, ← neg_add' (x ^ 2) 1, add_comm (x ^ 2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq]
  ring
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
⊢ ∀ (x : ℝ), HasDerivAt f (f' x) x
[PROOFSTEP]
intro x
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
⊢ HasDerivAt f (f' x) x
[PROOFSTEP]
have has_deriv_at_b : ∀ i ∈ Finset.range k, HasDerivAt (b i) ((-x ^ 2) ^ i) x :=
  by
  intro i _
  convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
  · ext y
    simp only [id.def]
    ring
  · simp
    rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
      mul_pow (-1 : ℝ) (x ^ 2) i]
    ring_nf
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
⊢ ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
[PROOFSTEP]
intro i _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ HasDerivAt (b i) ((-x ^ 2) ^ i) x
[PROOFSTEP]
convert HasDerivAt.const_mul ((-1 : ℝ) ^ i / (2 * i + 1)) (HasDerivAt.pow (2 * i + 1) (hasDerivAt_id x)) using 1
[GOAL]
case h.e'_6
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ b i = fun y => (-1) ^ i / (2 * ↑i + 1) * id y ^ (2 * i + 1)
[PROOFSTEP]
ext y
[GOAL]
case h.e'_6.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
y : ℝ
⊢ b i y = (-1) ^ i / (2 * ↑i + 1) * id y ^ (2 * i + 1)
[PROOFSTEP]
simp only [id.def]
[GOAL]
case h.e'_6.h
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
y : ℝ
⊢ (-1) ^ i * y ^ (2 * i + 1) / (2 * ↑i + 1) = (-1) ^ i / (2 * ↑i + 1) * y ^ (2 * i + 1)
[PROOFSTEP]
ring
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1) ^ i / (2 * ↑i + 1) * (↑(2 * i + 1) * id x ^ (2 * i + 1 - 1) * 1)
[PROOFSTEP]
simp
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1) ^ i / (2 * ↑i + 1) * ((2 * ↑i + 1) * x ^ (2 * i))
[PROOFSTEP]
rw [← mul_assoc, @div_mul_cancel _ _ (2 * (i : ℝ) + 1) _ (by norm_cast; linarith), pow_mul x 2 i, ←
  mul_pow (-1 : ℝ) (x ^ 2) i]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ 2 * ↑i + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ ¬2 * i + 1 = 0
[PROOFSTEP]
linarith
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
i : ℕ
a✝ : i ∈ Finset.range k
⊢ (-x ^ 2) ^ i = (-1 * x ^ 2) ^ i
[PROOFSTEP]
ring_nf
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
⊢ HasDerivAt f (f' x) x
[PROOFSTEP]
convert (hasDerivAt_arctan x).sub (HasDerivAt.sum has_deriv_at_b) using 1
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
⊢ f' x = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
have g_sum := @geom_sum_eq _ _ (-x ^ 2) ((neg_nonpos.mpr (sq_nonneg x)).trans_lt zero_lt_one).ne k
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ f' x = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
simp only at g_sum ⊢
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ (-x ^ 2) ^ k / (↑1 + x ^ 2) = ↑1 / (↑1 + x ^ 2) - ∑ i in Finset.range k, (-x ^ 2) ^ i
[PROOFSTEP]
rw [g_sum, ← neg_add' (x ^ 2) 1, add_comm (x ^ 2) 1, sub_eq_add_neg, neg_div', neg_div_neg_eq]
[GOAL]
case h.e'_7
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
x : ℝ
has_deriv_at_b : ∀ (i : ℕ), i ∈ Finset.range k → HasDerivAt (b i) ((-x ^ 2) ^ i) x
g_sum : ∑ i in Finset.range k, (-x ^ 2) ^ i = ((-x ^ 2) ^ k - 1) / (-x ^ 2 - 1)
⊢ (-x ^ 2) ^ k / (↑1 + x ^ 2) = ↑1 / (↑1 + x ^ 2) + ((-x ^ 2) ^ k - 1) / (1 + x ^ 2)
[PROOFSTEP]
ring
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hderiv1 : ∀ x ∈ Icc (U : ℝ) 1, HasDerivWithinAt f (f' x) (Icc (U : ℝ) 1) x := fun x _ =>
  (has_deriv_at_f x).hasDerivWithinAt
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hderiv2 : ∀ x ∈ Icc 0 (U : ℝ), HasDerivWithinAt f (f' x) (Icc 0 (U : ℝ)) x := fun x _ =>
  (has_deriv_at_f x).hasDerivWithinAt
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have f'_bound : ∀ x ∈ Icc (-1 : ℝ) 1, |f' x| ≤ |x| ^ (2 * k) :=
  by
  intro x _
  rw [abs_div, IsAbsoluteValue.abv_pow abs (-x ^ 2) k, abs_neg, IsAbsoluteValue.abv_pow abs x 2, ← pow_mul]
  refine' div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _
  refine' le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _
  rw_mod_cast [abs_of_nonneg (add_nonneg zero_le_one (sq_nonneg x) : (0 : ℝ) ≤ _)]
  exact (le_add_of_nonneg_right (sq_nonneg x) : (1 : ℝ) ≤ _)
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
⊢ ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
[PROOFSTEP]
intro x _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |f' x| ≤ |x| ^ (2 * k)
[PROOFSTEP]
rw [abs_div, IsAbsoluteValue.abv_pow abs (-x ^ 2) k, abs_neg, IsAbsoluteValue.abv_pow abs x 2, ← pow_mul]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |x| ^ (2 * k) / |↑1 + x ^ 2| ≤ |x| ^ (2 * k)
[PROOFSTEP]
refine' div_le_of_nonneg_of_le_mul (abs_nonneg _) (pow_nonneg (abs_nonneg _) _) _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ |x| ^ (2 * k) ≤ |x| ^ (2 * k) * |↑1 + x ^ 2|
[PROOFSTEP]
refine' le_mul_of_one_le_right (pow_nonneg (abs_nonneg _) _) _
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
a✝ : x ∈ Icc (-1) 1
⊢ 1 ≤ |↑1 + x ^ 2|
[PROOFSTEP]
rw_mod_cast [abs_of_nonneg (add_nonneg zero_le_one (sq_nonneg x) : (0 : ℝ) ≤ _)]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
x : ℝ
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * k + 1))) atTop (𝓝 0)
hU1 : U ≤ 1
hU2 : 0 ≤ U
a✝ : x ∈ Icc (↑(Int.negSucc 0)) 1
⊢ 1 ≤ 1 + x ^ 2
[PROOFSTEP]
exact (le_add_of_nonneg_right (sq_nonneg x) : (1 : ℝ) ≤ _)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hbound1 : ∀ x ∈ Ico (U : ℝ) 1, |f' x| ≤ 1 :=
  by
  rintro x ⟨hx_left, hx_right⟩
  have hincr := pow_le_pow_of_le_left (le_trans hU2 hx_left) (le_of_lt hx_right) (2 * k)
  rw [one_pow (2 * k), ← abs_of_nonneg (le_trans hU2 hx_left)] at hincr
  rw [← abs_of_nonneg (le_trans hU2 hx_left)] at hx_right
  linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_of_lt hx_right)))]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
⊢ ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
[PROOFSTEP]
rintro x ⟨hx_left, hx_right⟩
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
have hincr := pow_le_pow_of_le_left (le_trans hU2 hx_left) (le_of_lt hx_right) (2 * k)
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
hincr : x ^ (2 * k) ≤ 1 ^ (2 * k)
⊢ |f' x| ≤ 1
[PROOFSTEP]
rw [one_pow (2 * k), ← abs_of_nonneg (le_trans hU2 hx_left)] at hincr
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : x < 1
hincr : |x| ^ (2 * k) ≤ 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
rw [← abs_of_nonneg (le_trans hU2 hx_left)] at hx_right
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
x : ℝ
hx_left : ↑U ≤ x
hx_right : |x| < 1
hincr : |x| ^ (2 * k) ≤ 1
⊢ |f' x| ≤ 1
[PROOFSTEP]
linarith [f'_bound x (mem_Icc.mpr (abs_le.mp (le_of_lt hx_right)))]
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have hbound2 : ∀ x ∈ Ico 0 (U : ℝ), |f' x| ≤ U ^ (2 * k) :=
  by
  rintro x ⟨hx_left, hx_right⟩
  have hincr := pow_le_pow_of_le_left hx_left (le_of_lt hx_right) (2 * k)
  rw [← abs_of_nonneg hx_left] at hincr hx_right
  rw [← abs_of_nonneg hU2] at hU1 hx_right
  exact (f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))).trans hincr
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
⊢ ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rintro x ⟨hx_left, hx_right⟩
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : x < ↑U
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
have hincr := pow_le_pow_of_le_left hx_left (le_of_lt hx_right) (2 * k)
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : x < ↑U
hincr : x ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rw [← abs_of_nonneg hx_left] at hincr hx_right
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : |x| < ↑U
hincr : |x| ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
rw [← abs_of_nonneg hU2] at hU1 hx_right
[GOAL]
case intro
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : |↑U| ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
x : ℝ
hx_left : 0 ≤ x
hx_right : |x| < |↑U|
hincr : |x| ^ (2 * k) ≤ ↑U ^ (2 * k)
⊢ |f' x| ≤ ↑(U ^ (2 * k))
[PROOFSTEP]
exact (f'_bound x (mem_Icc.mpr (abs_le.mp (le_trans (le_of_lt hx_right) hU1)))).trans hincr
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have mvt1 := norm_image_sub_le_of_norm_deriv_le_segment' hderiv1 hbound1 _ (right_mem_Icc.mpr hU1)
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
have mvt2 :=
  norm_image_sub_le_of_norm_deriv_le_segment' hderiv2 hbound2 _
    (right_mem_Icc.mpr hU2)
      -- The following algebra is enough to complete the proof
[GOAL]
case f_bound
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ |f 1 - f 0| ≤ 1 - ↑U + ↑(U ^ (2 * ↑k + 1))
[PROOFSTEP]
calc
  |f 1 - f 0| = |f 1 - f U + (f U - f 0)| := by simp
  _ ≤ 1 * (1 - U) + U ^ (2 * k) * (U - 0) := (le_trans (abs_add (f 1 - f U) (f U - f 0)) (add_le_add mvt1 mvt2))
  _ = 1 - U + (U : ℝ) ^ (2 * k) * U := by simp
  _ = 1 - u k + u k ^ (2 * (k : ℝ) + 1) := by rw [← pow_succ' (U : ℝ) (2 * k)]; norm_cast
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ |f 1 - f 0| = |f 1 - f ↑U + (f ↑U - f 0)|
[PROOFSTEP]
simp
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 * (1 - ↑U) + ↑(U ^ (2 * k)) * (↑U - 0) = 1 - ↑U + ↑U ^ (2 * k) * ↑U
[PROOFSTEP]
simp
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 - ↑U + ↑U ^ (2 * k) * ↑U = 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
rw [← pow_succ' (U : ℝ) (2 * k)]
[GOAL]
u : ℕ → NNReal := fun k => ↑k ^ (-1 / (2 * ↑k + 1))
H : Tendsto (fun k => 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))) atTop (𝓝 0)
k : ℕ
U : NNReal := u k
b : ℕ → ℝ → ℝ := fun i x => (-1) ^ i * x ^ (2 * i + 1) / (2 * ↑i + 1)
f : ℝ → ℝ := fun x => arctan x - ∑ i in Finset.range k, b i x
hU1 : ↑U ≤ 1
hU2 : 0 ≤ ↑U
f' : ℝ → ℝ := fun x => (-x ^ 2) ^ k / (↑1 + x ^ 2)
has_deriv_at_f : ∀ (x : ℝ), HasDerivAt f (f' x) x
hderiv1 : ∀ (x : ℝ), x ∈ Icc (↑U) 1 → HasDerivWithinAt f (f' x) (Icc (↑U) 1) x
hderiv2 : ∀ (x : ℝ), x ∈ Icc 0 ↑U → HasDerivWithinAt f (f' x) (Icc 0 ↑U) x
f'_bound : ∀ (x : ℝ), x ∈ Icc (-1) 1 → |f' x| ≤ |x| ^ (2 * k)
hbound1 : ∀ (x : ℝ), x ∈ Ico (↑U) 1 → |f' x| ≤ 1
hbound2 : ∀ (x : ℝ), x ∈ Ico 0 ↑U → |f' x| ≤ ↑(U ^ (2 * k))
mvt1 : ‖f 1 - f ↑U‖ ≤ 1 * (1 - ↑U)
mvt2 : ‖f ↑U - f 0‖ ≤ ↑(U ^ (2 * k)) * (↑U - 0)
⊢ 1 - ↑U + ↑U ^ (2 * k + 1) = 1 - ↑(u k) + ↑(u k ^ (2 * ↑k + 1))
[PROOFSTEP]
norm_cast


[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
x : α
⊢ reverse (x ::ᵥ xs) = snoc (reverse xs) x
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (x ::ᵥ { val := val✝, property := property✝ }) = snoc (reverse { val := val✝, property := property✝ }) x
[PROOFSTEP]
simp only [reverse, cons, toList_mk, List.reverse_cons, snoc]
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ { val := List.reverse val✝ ++ [x],
      property := (_ : (fun l => List.length l = Nat.succ n) (List.reverse val✝ ++ [x])) } =
    append { val := List.reverse val✝, property := (_ : (fun l => List.length l = n) (List.reverse val✝)) }
      { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
x : α
⊢ reverse (snoc xs x) = x ::ᵥ reverse xs
[PROOFSTEP]
cases xs
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ reverse (snoc { val := val✝, property := property✝ } x) = x ::ᵥ reverse { val := val✝, property := property✝ }
[PROOFSTEP]
simp only [reverse, snoc, cons, toList_mk]
[GOAL]
case mk
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ {
      val :=
        List.reverse
          (toList
            (append { val := val✝, property := property✝ }
              { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })),
      property :=
        (_ :
          (fun l => List.length l = n + 1)
            (List.reverse
              (toList
                (append { val := val✝, property := property✝ }
                  { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })))) } =
    { val := x :: List.reverse val✝, property := (_ : Nat.succ (List.length (List.reverse val✝)) = Nat.succ n) }
[PROOFSTEP]
congr
[GOAL]
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ List.reverse
      (toList
        (append { val := val✝, property := property✝ }
          { val := [x], property := (_ : Nat.succ (List.length []) = Nat.succ 0) })) =
    x :: List.reverse val✝
[PROOFSTEP]
simp [toList, (· ++ ·), Vector.append, Append.append]
[GOAL]
case mk.e_val
α : Type u_1
n : ℕ
x : α
val✝ : List α
property✝ : List.length val✝ = n
⊢ [] ++ [x] ++ List.reverse val✝ = x :: List.reverse val✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
n : ℕ
xs : Vector α n
val : α
⊢ replicate (n + 1) val = snoc (replicate n val) val
[PROOFSTEP]
clear xs
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (n + 1) val = snoc (replicate n val) val
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
case succ
α : Type u_1
n : ℕ
val : α
n✝ : ℕ
n_ih✝ : replicate (n✝ + 1) val = snoc (replicate n✝ val) val
⊢ replicate (Nat.succ n✝ + 1) val = snoc (replicate (Nat.succ n✝) val) val
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
[PROOFSTEP]
case zero => rfl
[GOAL]
α : Type u_1
n : ℕ
val : α
⊢ replicate (Nat.zero + 1) val = snoc (replicate Nat.zero val) val
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
n : ℕ
val : α
n✝ : ℕ
n_ih✝ : replicate (n✝ + 1) val = snoc (replicate n✝ val) val
⊢ replicate (Nat.succ n✝ + 1) val = snoc (replicate (Nat.succ n✝) val) val
[PROOFSTEP]
case succ n ih =>
  rw [replicate_succ]
  conv => {rhs; rw [replicate_succ]}
  rw [snoc_cons, ih]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ replicate (Nat.succ n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
case succ n ih =>
  rw [replicate_succ]
  conv => {rhs; rw [replicate_succ]}
  rw [snoc_cons, ih]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ replicate (Nat.succ n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rw [replicate_succ]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
conv => {rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
{rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
{rhs; rw [replicate_succ]}
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| val ::ᵥ replicate (n + 1) val = snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
| snoc (replicate (Nat.succ n) val) val
[PROOFSTEP]
rw [replicate_succ]
[GOAL]
α : Type u_1
n✝ : ℕ
val : α
n : ℕ
ih : replicate (n + 1) val = snoc (replicate n val) val
⊢ val ::ᵥ replicate (n + 1) val = snoc (val ::ᵥ replicate n val) val
[PROOFSTEP]
rw [snoc_cons, ih]
[GOAL]
α : Type ?u.2475
C : {n : ℕ} → Vector α n → Sort u_1
n : ℕ
v : Vector α n
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (Vector.snoc xs x)
⊢ (fun {n} v => C (reverse v)) (reverse v) = C v
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2475
C : {n : ℕ} → Vector α n → Sort u_1
n✝ : ℕ
v : Vector α n✝
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (Vector.snoc xs x)
n : ℕ
x : α
xs : Vector α n
r : C (reverse xs)
⊢ C (Vector.snoc (reverse xs) x) = (fun {n} v => C (reverse v)) (x ::ᵥ xs)
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2985
β : Type ?u.2988
C : {n : ℕ} → Vector α n → Vector β n → Sort u_1
n : ℕ
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
snoc :
  {n : ℕ} →
    (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (Vector.snoc xs x) (Vector.snoc ys y)
⊢ (fun {n} v w => C (reverse v) (reverse w)) (reverse v) (reverse w) = C v w
[PROOFSTEP]
simp
[GOAL]
α : Type ?u.2985
β : Type ?u.2988
C : {n : ℕ} → Vector α n → Vector β n → Sort u_1
n✝ : ℕ
v : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
snoc :
  {n : ℕ} →
    (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (Vector.snoc xs x) (Vector.snoc ys y)
n : ℕ
x : α
y : β
xs : Vector α n
ys : Vector β n
r : C (reverse xs) (reverse ys)
⊢ C (Vector.snoc (reverse xs) x) (Vector.snoc (reverse ys) y) =
    (fun {n} v w => C (reverse v) (reverse w)) (x ::ᵥ xs) (y ::ᵥ ys)
[PROOFSTEP]
simp
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
⊢ map f (snoc xs x) = snoc (map f xs) (f x)
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
⊢ map f (snoc nil x) = snoc (map f nil) (f x)
[PROOFSTEP]
simp_all
[GOAL]
case h_cons
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type u_1
f : α → α✝
x : α
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ : map f (snoc w✝ x) = snoc (map f w✝) (f x)
⊢ map f (snoc (x✝ ::ᵥ w✝) x) = snoc (map f (x✝ ::ᵥ w✝)) (f x)
[PROOFSTEP]
simp_all
[GOAL]
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
⊢ mapAccumr f (snoc xs x) s =
    let q := f x s;
    let r := mapAccumr f xs q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
induction xs using Vector.inductionOn
[GOAL]
case h_nil
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
⊢ mapAccumr f (snoc nil x) s =
    let q := f x s;
    let r := mapAccumr f nil q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
rfl
[GOAL]
case h_cons
α : Type u_2
n : ℕ
xs : Vector α n
α✝ : Type
β✝ : Type u_1
f : α → α✝ → α✝ × β✝
x : α
s : α✝
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
a✝ :
  mapAccumr f (snoc w✝ x) s =
    let q := f x s;
    let r := mapAccumr f w✝ q.fst;
    (r.fst, snoc r.snd q.snd)
⊢ mapAccumr f (snoc (x✝ ::ᵥ w✝) x) s =
    let q := f x s;
    let r := mapAccumr f (x✝ ::ᵥ w✝) q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
⊢ map₂ f (snoc xs x) (snoc ys y) = snoc (map₂ f xs ys) (f x y)
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
⊢ map₂ f (snoc nil x) (snoc nil y) = snoc (map₂ f nil nil) (f x y)
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type u_2
n : ℕ
β : Type u_3
xs : Vector α n
ys : Vector β n
α✝ : Type u_1
f : α → β → α✝
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ : map₂ f (snoc x✝ x) (snoc y✝ y) = snoc (map₂ f x✝ y✝) (f x y)
⊢ map₂ f (snoc (a✝¹ ::ᵥ x✝) x) (snoc (b✝ ::ᵥ y✝) y) = snoc (map₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝)) (f x y)
[PROOFSTEP]
simp_all
[GOAL]
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (snoc xs x) (snoc ys y) c =
    let q := f x y c;
    let r := mapAccumr₂ f xs ys q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
induction xs, ys using Vector.inductionOn₂
[GOAL]
case nil
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
⊢ mapAccumr₂ f (snoc nil x) (snoc nil y) c =
    let q := f x y c;
    let r := mapAccumr₂ f nil nil q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp_all
[GOAL]
case cons
α : Type
n : ℕ
β : Type
xs : Vector α n
ys : Vector β n
σ φ : Type
c : σ
f : α → β → σ → σ × φ
x : α
y : β
n✝ : ℕ
a✝¹ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
a✝ :
  mapAccumr₂ f (snoc x✝ x) (snoc y✝ y) c =
    let q := f x y c;
    let r := mapAccumr₂ f x✝ y✝ q.fst;
    (r.fst, snoc r.snd q.snd)
⊢ mapAccumr₂ f (snoc (a✝¹ ::ᵥ x✝) x) (snoc (b✝ ::ᵥ y✝) y) c =
    let q := f x y c;
    let r := mapAccumr₂ f (a✝¹ ::ᵥ x✝) (b✝ ::ᵥ y✝) q.fst;
    (r.fst, snoc r.snd q.snd)
[PROOFSTEP]
simp_all


[GOAL]
⊢ φ⁻¹ = -ψ
[PROOFSTEP]
have : 1 + Real.sqrt 5 ≠ 0 := ne_of_gt (add_pos (by norm_num) <| Real.sqrt_pos.mpr (by norm_num))
[GOAL]
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 5
[PROOFSTEP]
norm_num
[GOAL]
this : 1 + sqrt 5 ≠ 0
⊢ φ⁻¹ = -ψ
[PROOFSTEP]
field_simp [sub_mul, mul_add]
[GOAL]
this : 1 + sqrt 5 ≠ 0
⊢ 2 * 2 = sqrt 5 * sqrt 5 - 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ⁻¹ = -φ
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]
[GOAL]
⊢ -ψ = φ⁻¹
[PROOFSTEP]
exact inv_gold.symm
[GOAL]
⊢ φ * ψ = -1
[PROOFSTEP]
field_simp
[GOAL]
⊢ (1 + sqrt 5) * (1 - sqrt 5) = -(2 * 2)
[PROOFSTEP]
rw [← sq_sub_sq]
[GOAL]
⊢ 1 ^ 2 - sqrt 5 ^ 2 = -(2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ * φ = -1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ φ * ψ = -1
[PROOFSTEP]
exact gold_mul_goldConj
[GOAL]
⊢ φ + ψ = 1
[PROOFSTEP]
rw [goldenRatio, goldenConj]
[GOAL]
⊢ (1 + sqrt 5) / 2 + (1 - sqrt 5) / 2 = 1
[PROOFSTEP]
ring
[GOAL]
⊢ 1 - φ = ψ
[PROOFSTEP]
linarith [gold_add_goldConj]
[GOAL]
⊢ 1 - ψ = φ
[PROOFSTEP]
linarith [gold_add_goldConj]
[GOAL]
⊢ φ - ψ = sqrt 5
[PROOFSTEP]
rw [goldenRatio, goldenConj]
[GOAL]
⊢ (1 + sqrt 5) / 2 - (1 - sqrt 5) / 2 = sqrt 5
[PROOFSTEP]
ring
[GOAL]
⊢ φ ^ 2 = φ + 1
[PROOFSTEP]
rw [goldenRatio, ← sub_eq_zero]
[GOAL]
⊢ ((1 + sqrt 5) / 2) ^ 2 - ((1 + sqrt 5) / 2 + 1) = 0
[PROOFSTEP]
ring_nf
[GOAL]
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
rw [Real.sq_sqrt]
[GOAL]
⊢ 5 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 ≤ 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ ^ 2 = ψ + 1
[PROOFSTEP]
rw [goldenConj, ← sub_eq_zero]
[GOAL]
⊢ ((1 - sqrt 5) / 2) ^ 2 - ((1 - sqrt 5) / 2 + 1) = 0
[PROOFSTEP]
ring_nf
[GOAL]
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
rw [Real.sq_sqrt]
[GOAL]
⊢ 5 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 ≤ 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 1 + sqrt 5
[PROOFSTEP]
apply add_pos
[GOAL]
case ha
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
case hb
⊢ 0 < sqrt 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ 1 < φ
[PROOFSTEP]
refine' lt_of_mul_lt_mul_left _ (le_of_lt gold_pos)
[GOAL]
⊢ φ * 1 < φ * φ
[PROOFSTEP]
simp [← sq, gold_pos, zero_lt_one, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
⊢ ψ < 0
[PROOFSTEP]
linarith [one_sub_goldConj, one_lt_gold]
[GOAL]
⊢ -1 < ψ
[PROOFSTEP]
rw [neg_lt, ← inv_gold]
[GOAL]
⊢ φ⁻¹ < 1
[PROOFSTEP]
exact inv_lt_one one_lt_gold
[GOAL]
⊢ Irrational φ
[PROOFSTEP]
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
[GOAL]
⊢ Nat.Prime 5
[PROOFSTEP]
norm_num
[GOAL]
this : Irrational (sqrt ↑5)
⊢ Irrational φ
[PROOFSTEP]
have := this.rat_add 1
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 + sqrt ↑5)
⊢ Irrational φ
[PROOFSTEP]
have := this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 + sqrt ↑5)
⊢ 0.5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ Irrational φ
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ φ = ↑0.5 * (↑1 + sqrt ↑5)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ φ = 1 / 2 * (1 + sqrt 5)
[PROOFSTEP]
field_simp
[GOAL]
⊢ Irrational ψ
[PROOFSTEP]
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
[GOAL]
⊢ Nat.Prime 5
[PROOFSTEP]
norm_num
[GOAL]
this : Irrational (sqrt ↑5)
⊢ Irrational ψ
[PROOFSTEP]
have := this.rat_sub 1
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ Irrational ψ
[PROOFSTEP]
have := this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ 0.5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ Irrational ψ
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ ψ = ↑0.5 * (↑1 - sqrt ↑5)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ ψ = 1 / 2 * (1 - sqrt 5)
[PROOFSTEP]
field_simp
[GOAL]
α : Type u_1
inst✝¹ : CommSemiring α
β : Type u_2
inst✝ : CommRing β
⊢ LinearRecurrence.charPoly fibRec = X ^ 2 - (X + 1)
[PROOFSTEP]
rw [fibRec, LinearRecurrence.charPoly]
[GOAL]
α : Type u_1
inst✝¹ : CommSemiring α
β : Type u_2
inst✝ : CommRing β
⊢ (↑(monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      Finset.sum Finset.univ fun i => ↑(monomial ↑i) (LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i)) =
    X ^ 2 - (X + 1)
[PROOFSTEP]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => ↑(Nat.fib x)
[PROOFSTEP]
rw [fibRec]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution { order := 2, coeffs := ![1, 1] } fun x => ↑(Nat.fib x)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    Finset.sum Finset.univ fun i =>
      LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i * (fun x => ↑(Nat.fib x)) (n + ↑i)
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
[PROOFSTEP]
rw [Nat.fib_add_two, add_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
[PROOFSTEP]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => φ ^ x
[PROOFSTEP]
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) φ
[PROOFSTEP]
simp [sub_eq_zero, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => ψ ^ x
[PROOFSTEP]
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) ψ
[PROOFSTEP]
simp [sub_eq_zero, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
⊢ (fun n => ↑(Nat.fib n)) = fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
rw [fibRec.sol_eq_of_eq_init]
[GOAL]
⊢ Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / sqrt 5) ↑(Finset.range fibRec.order)
[PROOFSTEP]
intro i hi
[GOAL]
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
[PROOFSTEP]
norm_cast at hi
[GOAL]
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
[PROOFSTEP]
fin_cases hi
[GOAL]
case head
⊢ (fun n => ↑(Nat.fib n)) 0 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 0
[PROOFSTEP]
simp
[GOAL]
case tail.head
⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 1
[PROOFSTEP]
simp only [goldenRatio, goldenConj]
[GOAL]
case tail.head
⊢ ↑(Nat.fib 1) = (((1 + sqrt 5) / 2) ^ 1 - ((1 - sqrt 5) / 2) ^ 1) / sqrt 5
[PROOFSTEP]
ring_nf
[GOAL]
case tail.head
⊢ 1 = sqrt 5 * (sqrt 5)⁻¹
[PROOFSTEP]
rw [mul_inv_cancel]
[GOAL]
case tail.head
⊢ sqrt 5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case hu
⊢ LinearRecurrence.IsSolution fibRec fun n => ↑(Nat.fib n)
[PROOFSTEP]
exact fib_isSol_fibRec
[GOAL]
case hv
⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
suffices LinearRecurrence.IsSolution fibRec ((fun n ↦ (sqrt 5)⁻¹ * φ ^ n) - (fun n ↦ (sqrt 5)⁻¹ * ψ ^ n))
  by
  convert this
  rw [Pi.sub_apply]
  ring
[GOAL]
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n) x✝
[PROOFSTEP]
rw [Pi.sub_apply]
[GOAL]
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = (sqrt 5)⁻¹ * φ ^ x✝ - (sqrt 5)⁻¹ * ψ ^ x✝
[PROOFSTEP]
ring
[GOAL]
case hv
⊢ LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
[PROOFSTEP]
apply (@fibRec ℝ _).solSpace.sub_mem
[GOAL]
case hv.a
⊢ (fun n => (sqrt 5)⁻¹ * φ ^ n) ∈ LinearRecurrence.solSpace fibRec
[PROOFSTEP]
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_gold_isSol_fibRec
[GOAL]
case hv.a
⊢ (fun n => (sqrt 5)⁻¹ * ψ ^ n) ∈ LinearRecurrence.solSpace fibRec
[PROOFSTEP]
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_goldConj_isSol_fibRec
[GOAL]
⊢ ∀ (n : ℕ), ↑(Nat.fib n) = (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
rw [← Function.funext_iff, Real.coe_fib_eq']


[GOAL]
p q : Primes
h : ↑p = ↑q
⊢ ↑p = ↑q
[PROOFSTEP]
injection h
[GOAL]
n m : ℕ+
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
let h := mul_pos n.pos m.pos
[GOAL]
n m : ℕ+
h : 0 < ↑n * ↑m := mul_pos (pos n) (pos m)
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
rw [← gcd_mul_lcm (n : ℕ) (m : ℕ), mul_comm] at h
[GOAL]
n m : ℕ+
h : 0 < Nat.lcm ↑n ↑m * Nat.gcd ↑n ↑m
⊢ 0 < Nat.lcm ↑n ↑m
[PROOFSTEP]
exact pos_of_dvd_of_pos (Dvd.intro (Nat.gcd (n : ℕ) (m : ℕ)) rfl) h
[GOAL]
n : ℕ+
⊢ n < 2 → n = 1
[PROOFSTEP]
intro h
[GOAL]
n : ℕ+
h : n < 2
⊢ n = 1
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
case a n : ℕ+ h : n < 2 ⊢ 1 ≤ n
[PROOFSTEP]
swap
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ 1 ≤ n
case a n : ℕ+ h : n < 2 ⊢ n ≤ 1
[PROOFSTEP]
apply PNat.one_le
[GOAL]
case a
n : ℕ+
h : n < 2
⊢ n ≤ 1
[PROOFSTEP]
exact PNat.lt_add_one_iff.1 h
[GOAL]
p m : ℕ+
pp : Prime p
⊢ m ∣ p ↔ m = 1 ∨ m = p
[PROOFSTEP]
rw [PNat.dvd_iff]
[GOAL]
p m : ℕ+
pp : Prime p
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
[PROOFSTEP]
rw [Nat.dvd_prime pp]
[GOAL]
p m : ℕ+
pp : Prime p
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
⊢ Prime p → p ≠ 1
[PROOFSTEP]
intro pp
[GOAL]
p : ℕ+
pp : Prime p
⊢ p ≠ 1
[PROOFSTEP]
intro contra
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ False
[PROOFSTEP]
apply Nat.Prime.ne_one pp
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ ↑p = 1
[PROOFSTEP]
rw [PNat.coe_eq_one_iff]
[GOAL]
p : ℕ+
pp : Prime p
contra : p = 1
⊢ p = 1
[PROOFSTEP]
apply contra
[GOAL]
p : ℕ+
pp : Prime p
⊢ ¬p ∣ 1
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
p : ℕ+
pp : Prime p
⊢ ¬↑p ∣ ↑1
[PROOFSTEP]
apply Nat.Prime.not_dvd_one pp
[GOAL]
n : ℕ+
hn : n ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, Prime p ∧ p ∣ n
[PROOFSTEP]
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ { val := p, property := (_ : 0 < p) } ∣ n
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime { val := p, property := (_ : 0 < p) } ∧ ↑{ val := p, property := (_ : 0 < p) } ∣ ↑n
[PROOFSTEP]
apply hp
[GOAL]
m n : ℕ+
⊢ coprime ↑m ↑n ↔ Coprime m n
[PROOFSTEP]
unfold coprime Coprime
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ gcd m n = 1
[PROOFSTEP]
rw [← coe_inj]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = 1 ↔ ↑(gcd m n) = ↑1
[PROOFSTEP]
simp
[GOAL]
k m n : ℕ+
⊢ Coprime m k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ Coprime m k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → Coprime n k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → Coprime (m * n) k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime ↑(m * n) ↑k
[PROOFSTEP]
rw [mul_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑m ↑k → coprime ↑n ↑k → coprime (↑m * ↑n) ↑k
[PROOFSTEP]
apply Nat.coprime.mul
[GOAL]
k m n : ℕ+
⊢ Coprime k m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ Coprime k m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → Coprime k n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → Coprime k (m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime ↑k ↑(m * n)
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime ↑k ↑(m * n)
[PROOFSTEP]
rw [mul_coe]
[GOAL]
k m n : ℕ+
⊢ coprime ↑k ↑m → coprime ↑k ↑n → coprime (↑k) (↑m * ↑n)
[PROOFSTEP]
apply Nat.coprime.mul_right
[GOAL]
m n : ℕ+
⊢ gcd m n = gcd n m
[PROOFSTEP]
apply eq
[GOAL]
case a
m n : ℕ+
⊢ ↑(gcd m n) = ↑(gcd n m)
[PROOFSTEP]
simp only [gcd_coe]
[GOAL]
case a
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = Nat.gcd ↑n ↑m
[PROOFSTEP]
apply Nat.gcd_comm
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd m n = m
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m n : ℕ+
⊢ ↑m ∣ ↑n ↔ gcd m n = m
[PROOFSTEP]
rw [Nat.gcd_eq_left_iff_dvd]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = ↑m ↔ gcd m n = m
[PROOFSTEP]
rw [← coe_inj]
[GOAL]
m n : ℕ+
⊢ Nat.gcd ↑m ↑n = ↑m ↔ ↑(gcd m n) = ↑m
[PROOFSTEP]
simp
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd n m = m
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n : ℕ+
⊢ m ∣ n ↔ gcd m n = m
[PROOFSTEP]
apply gcd_eq_left_iff_dvd
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
[PROOFSTEP]
intro h
[GOAL]
m n k : ℕ+
h : Coprime k n
⊢ gcd (k * m) n = gcd m n
[PROOFSTEP]
apply eq
[GOAL]
case a
m n k : ℕ+
h : Coprime k n
⊢ ↑(gcd (k * m) n) = ↑(gcd m n)
[PROOFSTEP]
simp only [gcd_coe, mul_coe]
[GOAL]
case a
m n k : ℕ+
h : Coprime k n
⊢ Nat.gcd (↑k * ↑m) ↑n = Nat.gcd ↑m ↑n
[PROOFSTEP]
apply Nat.coprime.gcd_mul_left_cancel
[GOAL]
case a.H
m n k : ℕ+
h : Coprime k n
⊢ coprime ↑k ↑n
[PROOFSTEP]
simpa
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (m * k) n = gcd m n
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k : ℕ+
⊢ Coprime k n → gcd (k * m) n = gcd m n
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (k * n) = gcd m n
[PROOFSTEP]
intro h
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
[PROOFSTEP]
iterate 2 rw [gcd_comm]; symm;
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m (k * n) = gcd m n
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd m n
[PROOFSTEP]
symm
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd m n = gcd (k * n) m
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd n m = gcd (k * n) m
[PROOFSTEP]
symm
[GOAL]
m n k : ℕ+
h : Coprime k m
⊢ gcd (k * n) m = gcd n m
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel _ h
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (n * k) = gcd m n
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k : ℕ+
⊢ Coprime k m → gcd m (k * n) = gcd m n
[PROOFSTEP]
apply Coprime.gcd_mul_left_cancel_right
[GOAL]
n : ℕ+
⊢ gcd 1 n = 1
[PROOFSTEP]
rw [← gcd_eq_left_iff_dvd]
[GOAL]
n : ℕ+
⊢ 1 ∣ n
[PROOFSTEP]
apply one_dvd
[GOAL]
n : ℕ+
⊢ gcd n 1 = 1
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
n : ℕ+
⊢ gcd 1 n = 1
[PROOFSTEP]
apply one_gcd
[GOAL]
m n : ℕ+
⊢ Coprime m n → Coprime n m
[PROOFSTEP]
unfold Coprime
[GOAL]
m n : ℕ+
⊢ gcd m n = 1 → gcd n m = 1
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
m n : ℕ+
⊢ gcd n m = 1 → gcd n m = 1
[PROOFSTEP]
simp
[GOAL]
m k n : ℕ+
⊢ m ∣ k → Coprime k n → Coprime m n
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
[PROOFSTEP]
repeat' rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → Coprime k n → Coprime m n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → Coprime m n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
[PROOFSTEP]
rw [← coprime_coe]
[GOAL]
m k n : ℕ+
⊢ ↑m ∣ ↑k → coprime ↑k ↑n → coprime ↑m ↑n
[PROOFSTEP]
apply Nat.coprime.coprime_dvd_left
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
rw [gcd_eq_left_iff_dvd] at am
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
conv_lhs => rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
| a
[PROOFSTEP]
rw [← am]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd a m = gcd (a * b) m
[PROOFSTEP]
rw [eq_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ gcd (a * b) m = gcd a m
[PROOFSTEP]
apply Coprime.gcd_mul_right_cancel a
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : gcd a m = a
bn : b ∣ n
⊢ Coprime b m
[PROOFSTEP]
apply Coprime.coprime_dvd_left bn cop.symm
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (b * a) m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_left cop am bn
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd m (a * b)
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (a * b) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_left cop am bn
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd m (b * a)
[PROOFSTEP]
rw [gcd_comm]
[GOAL]
a b m n : ℕ+
cop : Coprime m n
am : a ∣ m
bn : b ∣ n
⊢ a = gcd (b * a) m
[PROOFSTEP]
apply Coprime.factor_eq_gcd_right cop am bn
[GOAL]
k m n : ℕ+
h : Coprime m n
⊢ gcd k (m * n) = gcd k m * gcd k n
[PROOFSTEP]
rw [← coprime_coe] at h
[GOAL]
k m n : ℕ+
h : coprime ↑m ↑n
⊢ gcd k (m * n) = gcd k m * gcd k n
[PROOFSTEP]
apply eq
[GOAL]
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ ↑(gcd k (m * n)) = ↑(gcd k m * gcd k n)
[PROOFSTEP]
simp only [gcd_coe, mul_coe]
[GOAL]
case a
k m n : ℕ+
h : coprime ↑m ↑n
⊢ Nat.gcd (↑k) (↑m * ↑n) = Nat.gcd ↑k ↑m * Nat.gcd ↑k ↑n
[PROOFSTEP]
apply Nat.coprime.gcd_mul k h
[GOAL]
m n : ℕ+
⊢ m ∣ n → gcd m n = m
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
m n : ℕ+
⊢ ↑m ∣ ↑n → gcd m n = m
[PROOFSTEP]
intro h
[GOAL]
m n : ℕ+
h : ↑m ∣ ↑n
⊢ gcd m n = m
[PROOFSTEP]
apply eq
[GOAL]
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ ↑(gcd m n) = ↑m
[PROOFSTEP]
simp only [gcd_coe]
[GOAL]
case a
m n : ℕ+
h : ↑m ∣ ↑n
⊢ Nat.gcd ↑m ↑n = ↑m
[PROOFSTEP]
apply Nat.gcd_eq_left h
[GOAL]
m n : ℕ+
k l : ℕ
h : Coprime m n
⊢ coprime (↑m ^ k) (↑n ^ l)
[PROOFSTEP]
rw [← coprime_coe] at *
[GOAL]
m n : ℕ+
k l : ℕ
h : coprime ↑m ↑n
⊢ coprime (↑m ^ k) (↑n ^ l)
[PROOFSTEP]
apply Nat.coprime.pow
[GOAL]
case H1
m n : ℕ+
k l : ℕ
h : coprime ↑m ↑n
⊢ coprime ↑m ↑n
[PROOFSTEP]
apply h


[GOAL]
n : ℕ+
⊢ 1 + natPred n = ↑n
[PROOFSTEP]
rw [natPred, add_tsub_cancel_iff_le.mpr <| show 1 ≤ (n : ℕ) from n.2]
[GOAL]
a b : ℕ+
⊢ ↑(a - b) = if b < a then ↑a - ↑b else 1
[PROOFSTEP]
change (toPNat' _ : ℕ) = ite _ _ _
[GOAL]
a b : ℕ+
⊢ ↑(toPNat' (↑a - ↑b)) = if b < a then ↑a - ↑b else 1
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
a b : ℕ+
h : b < a
⊢ ↑(toPNat' (↑a - ↑b)) = ↑a - ↑b
[PROOFSTEP]
exact toPNat'_coe (tsub_pos_of_lt h)
[GOAL]
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' (↑a - ↑b)) = 1
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr (le_of_not_gt h : (a : ℕ) ≤ b)]
[GOAL]
case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(toPNat' 0) = 1
[PROOFSTEP]
rfl
[GOAL]
a b : ℕ+
h : a < b
⊢ ↑(a + (b - a)) = ↑b
[PROOFSTEP]
rw [add_coe, sub_coe, if_pos h]
[GOAL]
a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b
[PROOFSTEP]
exact add_tsub_cancel_of_le h.le
[GOAL]
n : ℕ
property✝ : 0 < n + 2
x✝ : { val := n + 2, property := property✝ } ≠ 1
⊢ 0 < n + 1
[PROOFSTEP]
simp
[GOAL]
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ p a
[PROOFSTEP]
apply strongInductionOn a
[GOAL]
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
⊢ (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k
[PROOFSTEP]
rintro ⟨k, kprop⟩ hk
[GOAL]
case mk
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k
hk : (m : ℕ+) → m < { val := k, property := kprop } → p m
⊢ p { val := k, property := kprop }
[PROOFSTEP]
cases' k with k
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < zero
hk : (m : ℕ+) → m < { val := zero, property := kprop } → p m
⊢ p { val := zero, property := kprop }
[PROOFSTEP]
exact (lt_irrefl 0 kprop).elim
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < succ k
hk : (m : ℕ+) → m < { val := succ k, property := kprop } → p m
⊢ p { val := succ k, property := kprop }
[PROOFSTEP]
cases' k with k
[GOAL]
case mk.succ.zero
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
kprop : 0 < succ zero
hk : (m : ℕ+) → m < { val := succ zero, property := kprop } → p m
⊢ p { val := succ zero, property := kprop }
[PROOFSTEP]
exact hz
[GOAL]
case mk.succ.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < succ (succ k)
hk : (m : ℕ+) → m < { val := succ (succ k), property := kprop } → p m
⊢ p { val := succ (succ k), property := kprop }
[PROOFSTEP]
exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (lt_succ_iff.2 hm)
[GOAL]
n : ℕ+
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
⊢ p n
[PROOFSTEP]
rcases n with ⟨n, h⟩
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ p { val := n, property := h }
[PROOFSTEP]
induction' n with n IH
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
h : 0 < zero
⊢ p { val := zero, property := h }
[PROOFSTEP]
exact absurd h (by decide)
[GOAL]
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
h : 0 < zero
⊢ ¬0 < zero
[PROOFSTEP]
decide
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h✝ : 0 < n✝
n : ℕ
IH : (h : 0 < n) → p { val := n, property := h }
h : 0 < succ n
⊢ p { val := succ n, property := h }
[PROOFSTEP]
cases' n with n
[GOAL]
case mk.succ.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h✝ : 0 < n
IH : (h : 0 < zero) → p { val := zero, property := h }
h : 0 < succ zero
⊢ p { val := succ zero, property := h }
[PROOFSTEP]
exact p1
[GOAL]
case mk.succ.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h✝ : 0 < n✝
n : ℕ
IH : (h : 0 < succ n) → p { val := succ n, property := h }
h : 0 < succ (succ n)
⊢ p { val := succ (succ n), property := h }
[PROOFSTEP]
exact hp _ (IH n.succ_pos)
[GOAL]
n : ℕ+
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
⊢ recOn (n + 1) p1 hp = hp n (recOn n p1 hp)
[PROOFSTEP]
cases' n with n h
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ recOn ({ val := n, property := h } + 1) p1 hp =
    hp { val := n, property := h } (recOn { val := n, property := h } p1 hp)
[PROOFSTEP]
cases n <;> [exact absurd h (by decide); rfl]
[GOAL]
case mk
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ recOn ({ val := n, property := h } + 1) p1 hp =
    hp { val := n, property := h } (recOn { val := n, property := h } p1 hp)
[PROOFSTEP]
cases n
[GOAL]
case mk.zero
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
h : 0 < zero
⊢ recOn ({ val := zero, property := h } + 1) p1 hp =
    hp { val := zero, property := h } (recOn { val := zero, property := h } p1 hp)
[PROOFSTEP]
exact absurd h (by decide)
[GOAL]
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
h : 0 < zero
⊢ ¬0 < zero
[PROOFSTEP]
decide
[GOAL]
case mk.succ
p : ℕ+ → Sort u_1
p1 : p 1
hp : (n : ℕ+) → p n → p (n + 1)
n✝ : ℕ
h : 0 < succ n✝
⊢ recOn ({ val := succ n✝, property := h } + 1) p1 hp =
    hp { val := succ n✝, property := h } (recOn { val := succ n✝, property := h } p1 hp)
[PROOFSTEP]
rfl
[GOAL]
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑(modDivAux k 0 (q + 1)).fst + ↑k * (modDivAux k 0 (q + 1)).snd = 0 + ↑k * (q + 1)
[PROOFSTEP]
change (k : ℕ) + (k : ℕ) * (q + 1).pred = 0 + (k : ℕ) * (q + 1)
[GOAL]
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * pred (q + 1) = 0 + ↑k * (q + 1)
[PROOFSTEP]
rw [Nat.pred_succ, Nat.mul_succ, zero_add, add_comm]
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
let h₀ := Nat.mod_add_div (m : ℕ) (k : ℕ)
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
have : ¬((m : ℕ) % (k : ℕ) = 0 ∧ (m : ℕ) / (k : ℕ) = 0) :=
  by
  rintro ⟨hr, hq⟩
  rw [hr, hq, mul_zero, zero_add] at h₀
  exact (m.ne_zero h₀.symm).elim
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
⊢ ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
[PROOFSTEP]
rintro ⟨hr, hq⟩
[GOAL]
case intro
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
[PROOFSTEP]
rw [hr, hq, mul_zero, zero_add] at h₀
[GOAL]
case intro
m k : ℕ+
h₀ : 0 = ↑m
hr : ↑m % ↑k = 0
hq : ↑m / ↑k = 0
⊢ False
[PROOFSTEP]
exact (m.ne_zero h₀.symm).elim
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
have := modDivAux_spec k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ)) this
[GOAL]
m k : ℕ+
h₀ : ↑m % ↑k + ↑k * (↑m / ↑k) = ↑m := Nat.mod_add_div ↑m ↑k
this✝ : ¬(↑m % ↑k = 0 ∧ ↑m / ↑k = 0)
this : ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst + ↑k * (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = ↑m % ↑k + ↑k * (↑m / ↑k)
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
exact this.trans h₀
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + div m k * ↑k = ↑m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) + ↑k * div m k = ↑m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
m k : ℕ+
⊢ div m k * ↑k + ↑(mod m k) = ↑m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m k : ℕ+
⊢ ↑k * div m k + ↑(mod m k) = ↑m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
m k : ℕ+
⊢ mod m k ≤ m ∧ mod m k ≤ k
[PROOFSTEP]
change (mod m k : ℕ) ≤ (m : ℕ) ∧ (mod m k : ℕ) ≤ (k : ℕ)
[GOAL]
m k : ℕ+
⊢ ↑(mod m k) ≤ ↑m ∧ ↑(mod m k) ≤ ↑k
[PROOFSTEP]
rw [mod_coe]
[GOAL]
m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k
[PROOFSTEP]
have hm : (m : ℕ) > 0 := m.pos
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m > 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
by_cases h₁ : (m : ℕ) / (k : ℕ) = 0
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [h₁, mul_zero] at hm
[GOAL]
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : 0 > 0
h₁ : ↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
exact (lt_irrefl _ hm).elim
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
let h₂ : (k : ℕ) * 1 ≤ k * (m / k) :=
  -- Porting note : Specified type of `h₂` explicitly because `rw` could not unify
          -- `succ 0` with `1`.Nat.mul_le_mul_left (k : ℕ) (Nat.succ_le_of_lt (Nat.pos_of_ne_zero h₁))
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k * 1 ≤ ↑k * (↑m / ↑k) := Nat.mul_le_mul_left (↑k) (succ_le_of_lt (Nat.pos_of_ne_zero h₁))
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
rw [mul_one] at h₂
[GOAL]
case neg
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑k * (↑m / ↑k) > 0
h₁ : ¬↑m / ↑k = 0
h₂ : ↑k ≤ ↑k * (↑m / ↑k)
⊢ ↑k ≤ ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
[PROOFSTEP]
exact ⟨h₂, le_refl (k : ℕ)⟩
[GOAL]
case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k
[PROOFSTEP]
exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩
[GOAL]
k m : ℕ+
⊢ k ∣ m ↔ ↑k ∣ ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m
[PROOFSTEP]
intro h
[GOAL]
case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m
[PROOFSTEP]
intro h
[GOAL]
case mp
k m : ℕ+
h : k ∣ m
⊢ ↑k ∣ ↑m
[PROOFSTEP]
rcases h with ⟨_, rfl⟩
[GOAL]
case mp.intro
k w✝ : ℕ+
⊢ ↑k ∣ ↑(k * w✝)
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
case mpr
k m : ℕ+
h : ↑k ∣ ↑m
⊢ k ∣ m
[PROOFSTEP]
rcases h with ⟨a, h⟩
[GOAL]
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
[PROOFSTEP]
cases a with
| zero =>
  contrapose h
  apply ne_zero
| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro
k m : ℕ+
a : ℕ
h : ↑m = ↑k * a
⊢ k ∣ m
[PROOFSTEP]
cases a with
| zero =>
  contrapose h
  apply ne_zero
| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ↑m = ↑k * zero
⊢ k ∣ m
[PROOFSTEP]

| zero =>
  contrapose h
  apply ne_zero
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ↑m = ↑k * zero
⊢ k ∣ m
[PROOFSTEP]
contrapose h
[GOAL]
case mpr.intro.zero
k m : ℕ+
h : ¬k ∣ m
⊢ ¬↑m = ↑k * zero
[PROOFSTEP]
apply ne_zero
[GOAL]
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ k ∣ m
[PROOFSTEP]

| succ n =>
  use⟨n.succ, n.succ_pos⟩
  rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
case mpr.intro.succ
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ k ∣ m
[PROOFSTEP]
use⟨n.succ, n.succ_pos⟩
[GOAL]
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * succ n
⊢ m = k * { val := succ n, property := (_ : 0 < succ n) }
[PROOFSTEP]
rw [← coe_inj, h, mul_coe, mk_coe]
[GOAL]
k m : ℕ+
⊢ k ∣ m ↔ mod m k = k
[PROOFSTEP]
rw [dvd_iff]
[GOAL]
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ mod m k = k
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero]
[GOAL]
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ mod m k = k
[PROOFSTEP]
constructor
[GOAL]
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → mod m k = k
[PROOFSTEP]
intro h
[GOAL]
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ mod m k = k
[PROOFSTEP]
apply PNat.eq
[GOAL]
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(mod m k) = ↑k
[PROOFSTEP]
rw [mod_coe, if_pos h]
[GOAL]
case mpr
k m : ℕ+
⊢ mod m k = k → ↑m % ↑k = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
k m : ℕ+
h : mod m k = k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
by_cases h' : (m : ℕ) % (k : ℕ) = 0
[GOAL]
case pos
k m : ℕ+
h : mod m k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0
[PROOFSTEP]
exact h'
[GOAL]
case neg
k m : ℕ+
h : mod m k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0
[PROOFSTEP]
replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
[GOAL]
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(mod m k) = ↑k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
rw [mod_coe, if_neg h'] at h
[GOAL]
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0
[PROOFSTEP]
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim
[GOAL]
m n : ℕ+
⊢ m ∣ n → m ≤ n
[PROOFSTEP]
rw [dvd_iff']
[GOAL]
m n : ℕ+
⊢ mod n m = m → m ≤ n
[PROOFSTEP]
intro h
[GOAL]
m n : ℕ+
h : mod n m = m
⊢ m ≤ n
[PROOFSTEP]
rw [← h]
[GOAL]
m n : ℕ+
h : mod n m = m
⊢ mod n m ≤ n
[PROOFSTEP]
apply (mod_le n m).left
[GOAL]
m k : ℕ+
h : k ∣ m
⊢ k * divExact m k = m
[PROOFSTEP]
apply PNat.eq
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * divExact m k) = ↑m
[PROOFSTEP]
rw [mul_coe]
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(divExact m k) = ↑m
[PROOFSTEP]
change (k : ℕ) * (div m k).succ = m
[GOAL]
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * succ (div m k) = ↑m
[PROOFSTEP]
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ 0 < a
[PROOFSTEP]
apply pos_iff_ne_zero.2
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
⊢ a ≠ 0
[PROOFSTEP]
intro hzero
[GOAL]
n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False
[PROOFSTEP]
rw [hzero] at h
[GOAL]
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
[PROOFSTEP]
exact PNat.ne_zero n (eq_zero_of_zero_dvd h)