awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
⊢ y ∈ f '' closedBall b ε
have D : ∀ (n : ℕ),
  dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
    dist (u n) b ≤
      (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
        dist (f b) y
Tactic: have D : ∀ n : ℕ, dist (f (u n)) y ≤ ((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) /
        (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y := fun n ↦ by
    induction n with
    | zero => simp [hu]
    | succ n IH => ?_
    rw [usucc]
    have Ign : dist (g (u n)) b ≤ f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) /
        (1 - c * f'symm.nnnorm) * dist (f b) y :=
      calc
        dist (g (u n)) b ≤ dist (g (u n)) (u n) + dist (u n) b := dist_triangle _ _ _
        _ ≤ f'symm.nnnorm * dist (f (u n)) y + dist (u n) b := add_le_add (A _) le_rfl
        _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) +
              f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n) / (1 - c * f'symm.nnnorm) *
                dist (f b) y := by
                  gcongr
                  · exact IH.1
                  · exact IH.2
        _ = f'symm.nnnorm * (1 - ((c : ℝ) * f'symm.nnnorm) ^ n.succ) /
              (1 - (c : ℝ) * f'symm.nnnorm) * dist (f b) y := by
          replace Jcf' : (1 : ℝ) - f'symm.nnnorm * c ≠ 0 := by convert! Jcf' using 1; ring
          simp [field, pow_succ, -mul_eq_mul_left_iff]
          ring
    refine ⟨?_, Ign⟩
    calc
      dist (f (g (u n))) y ≤ c * f'symm.nnnorm * dist (f (u n)) y :=
        B _ (C n _ IH.2) (C n.succ _ Ign)
      _ ≤ (c : ℝ) * f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        apply IH.1
      _ = ((c : ℝ) * f'symm.nnnorm) ^ n.succ * dist (f b) y := by simp only [pow_succ']; ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
⊢ CauchySeq u
have refine : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (↑f'symm.nnnorm : ℝ) * dist (f b) y * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
Tactic: refine cauchySeq_of_le_geometric _ (↑f'symm.nnnorm * dist (f b) y) Icf' fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
n : ℕ
⊢ dist (u n) (u (n + 1)) = dist (g (u n)) (u n)
have rw : dist (u n) (g (u n)) = dist (g (u n)) (u n)
Tactic: rw [usucc, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
n : ℕ
rw : dist (u n) (g (u n)) = dist (g (u n)) (u n)
⊢ dist (u n) (u (n + 1)) = dist (g (u n)) (u n)
have rw₁ : dist (g (u n)) (u n) = dist (g (u n)) (u n)
Tactic: rw [usucc, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
n : ℕ
⊢ (↑f'symm.nnnorm : ℝ) * dist (f (u n)) y ≤
    (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y)
have hbc : dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
n : ℕ
⊢ dist (u n) (u (n + 1)) ≤ (↑f'symm.nnnorm : ℝ) * dist (f b) y * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
have dist : dist (u n) (u (n + 1)) = dist (g (u n)) (u n)
Tactic: calc
      dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
      _ ≤ f'symm.nnnorm * dist (f (u n)) y := A _
      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        exact (D n).1
      _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), Dist.dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y
B :
  ∀ z ∈ closedBall b ε,
    g z ∈ closedBall b ε → Dist.dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    Dist.dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          Dist.dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    Dist.dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y ∧
      Dist.dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          Dist.dist (f b) y
n : ℕ
dist : Dist.dist (u n) (u (n + 1)) = Dist.dist (g (u n)) (u n)
⊢ Dist.dist (u n) (u (n + 1)) ≤ (↑f'symm.nnnorm : ℝ) * Dist.dist (f b) y * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
have dist₁ : (↑f'symm.nnnorm : ℝ) * Dist.dist (f (u n)) y ≤
  (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y)
Tactic: calc
      dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
      _ ≤ f'symm.nnnorm * dist (f (u n)) y := A _
      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        exact (D n).1
      _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), Dist.dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y
B :
  ∀ z ∈ closedBall b ε,
    g z ∈ closedBall b ε → Dist.dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    Dist.dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          Dist.dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    Dist.dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y ∧
      Dist.dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          Dist.dist (f b) y
n : ℕ
dist : Dist.dist (u n) (u (n + 1)) = Dist.dist (g (u n)) (u n)
dist₁ :
  (↑f'symm.nnnorm : ℝ) * Dist.dist (f (u n)) y ≤
    (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y)
⊢ Dist.dist (u n) (u (n + 1)) ≤ (↑f'symm.nnnorm : ℝ) * Dist.dist (f b) y * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
have dist₂ : (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y) =
  (↑f'symm.nnnorm : ℝ) * Dist.dist (f b) y * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
Tactic: calc
      dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
      _ ≤ f'symm.nnnorm * dist (f (u n)) y := A _
      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        exact (D n).1
      _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
⊢ y ∈ f '' closedBall b ε
have this : CauchySeq u
Tactic: have : CauchySeq u := by
    refine cauchySeq_of_le_geometric _ (↑f'symm.nnnorm * dist (f b) y) Icf' fun n ↦ ?_
    calc
      dist (u n) (u (n + 1)) = dist (g (u n)) (u n) := by rw [usucc, dist_comm]
      _ ≤ f'symm.nnnorm * dist (f (u n)) y := A _
      _ ≤ f'symm.nnnorm * (((c : ℝ) * f'symm.nnnorm) ^ n * dist (f b) y) := by
        gcongr
        exact (D n).1
      _ = f'symm.nnnorm * dist (f b) y * ((c : ℝ) * f'symm.nnnorm) ^ n := by ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
this : CauchySeq u
⊢ y ∈ f '' closedBall b ε
have inr : ∀ (x : E) (hx : Tendsto u atTop (𝓝 x)), y ∈ f '' closedBall b ε
Tactic: obtain ⟨x, hx⟩ : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹
If' : 0 < (↑f'symm.nnnorm : ℝ)
Icf' : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x)
hg : g = fun (x : E) ↦ x + f'symm.toFun (y - f x)
u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b
hu : u = fun (n : ℕ) ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y ∧
      dist (u n) b ≤
        (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
          dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
⊢ y ∈ f '' closedBall b ε
have xmem : x ∈ closedBall b ε
Tactic: have xmem : x ∈ closedBall b ε :=
    isClosed_closedBall.mem_of_tendsto hx (Eventually.of_forall fun n => C n _ (D n).2)