awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ε
n : ℕ
IH :
  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
⊢ (↑f'symm.nnnorm : ℝ) * dist (f (u n)) y + dist (u n) b ≤
    (↑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
have h₁ : 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 ε
n : ℕ
IH :
  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
h₁ : dist (f (u n)) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y
⊢ (↑f'symm.nnnorm : ℝ) * dist (f (u n)) y + dist (u n) b ≤
    (↑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
have h₂ : dist (u n) b ≤
  (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
    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 ε
n : ℕ
IH :
  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
⊢ 1 - (↑f'symm.nnnorm : ℝ) * (↑c : ℝ) ≠ 0
have h : 1 - (↑f'symm.nnnorm : ℝ) * (↑c : ℝ) = 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)
Tactic: convert! Jcf' using 1
-- 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 ε
n : ℕ
IH :
  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
⊢ (↑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 =
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n.succ) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
have Jcf'₁ : 1 - (↑f'symm.nnnorm : ℝ) * (↑c : ℝ) ≠ 0
Tactic: replace Jcf' : (1 : ℝ) - f'symm.nnnorm * c ≠ 0 := by convert! Jcf' using 1; ring
Cleared hypotheses: Jcf'
-- 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
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 ε
n : ℕ
IH :
  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
Jcf' : 1 - (↑f'symm.nnnorm : ℝ) * (↑c : ℝ) ≠ 0
⊢ (↑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 =
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n.succ) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
have simp : dist (f b) y *
    (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * (1 - (↑f'symm.nnnorm : ℝ) * (↑c : ℝ)) +
      (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n)) =
  dist (f b) y * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * (↑f'symm.nnnorm : ℝ) * (↑c : ℝ))
Tactic: simp [field, pow_succ, -mul_eq_mul_left_iff]
-- 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 ε
n : ℕ
IH :
  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
⊢ dist (f (g (u n))) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1) * dist (f b) y ∧
    dist (g (u n)) b ≤
      (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1)) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
        dist (f b) y
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
Tactic: 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
-- 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 ε
n : ℕ
IH :
  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
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
⊢ dist (f (g (u n))) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1) * dist (f b) y ∧
    dist (g (u n)) b ≤
      (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1)) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
        dist (f b) y
have succ : dist (f (g (u n))) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1) * dist (f b) y
Tactic: refine ⟨?_, Ign⟩
-- 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 ε
n : ℕ
IH :
  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
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
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f (u n)) y ≤
    (↑c : ℝ) * (↑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 ε
n : ℕ
IH :
  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
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
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y) =
    ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n.succ * dist (f b) y
have simp : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y) =
  (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y
Tactic: simp only [pow_succ']
-- 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 ε
n : ℕ
IH :
  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
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
⊢ dist (f (g (u n))) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1) * dist (f b) y
have dist : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f (u n)) y ≤
  (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y)
Tactic: 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.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 ε
n : ℕ
IH :
  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
Ign :
  Dist.dist (g (u n)) b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n.succ) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      Dist.dist (f b) y
dist :
  (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * Dist.dist (f (u n)) y ≤
    (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y)
⊢ Dist.dist (f (g (u n))) y ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ (n + 1) * Dist.dist (f b) y
have dist₁ : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * Dist.dist (f b) y) =
  ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n.succ * Dist.dist (f b) y
Tactic: 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