awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ‖HAdd.hAdd (β := F) (HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) v : F)) ((f' : (a : E) → F) v : F) -
        (y - f z)‖ =
    ‖HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) (z + v - z) : F)‖

Tactic:
simp only [v, ContinuousLinearMap.NonlinearRightInverse.right_inv, add_sub_cancel_left,
          sub_add_cancel]

Premises used: add_sub_cancel_left, ContinuousLinearMap.NonlinearRightInverse.right_inv, sub_add_cancel
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ‖HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) (z + v - z) : F)‖ ≤ (↑c : ℝ) * ‖z + v - z‖

Tactic:
hf _ (hε hgz) _ (hε hz)
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
hbc : ‖z + v - z‖ ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
⊢ (↑c : ℝ) * ‖z + v - z‖ ≤ (↑c : ℝ) * ((↑f'symm.nnnorm : ℝ) * dist (f z) y)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ ‖z + v - z‖ ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y

Tactic:
simpa [dist_eq_norm'] using f'symm.bound (y - f z)

Premises used: HSub.hSub, dist_eq_norm', ContinuousLinearMap.NonlinearRightInverse.bound
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
⊢ (↑c : ℝ) * ((↑f'symm.nnnorm : ℝ) * dist (f z) y) = (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
z : E
hz : z ∈ closedBall b ε
hgz : g z ∈ closedBall b ε
v : E := f'symm.toFun (y - f z)
dist : Dist.dist (f (g z)) y = ‖f (z + v) - y‖
dist₁ :
  ‖f (z + v) - y‖ =
    ‖HAdd.hAdd (β := F) (HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) v : F)) ((f' : (a : E) → F) v : F) -
        (y - f z)‖
dist₂ :
  ‖HAdd.hAdd (β := F) (HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) v : F)) ((f' : (a : E) → F) v : F) -
        (y - f z)‖ =
    ‖HSub.hSub (β := F) (f (z + v) - f z) ((f' : (a : E) → F) (z + v - z) : F)‖
dist₃ : (↑c : ℝ) * ‖z + v - z‖ ≤ (↑c : ℝ) * ((↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y)
dist₄ : (↑c : ℝ) * ((↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y) = (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y
⊢ Dist.dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * Dist.dist (f z) y

Tactic:
calc
      dist (f (g z)) y = ‖f (z + v) - y‖ := by rw [dist_eq_norm]
      _ = ‖f (z + v) - f z - f' v + f' v - (y - f z)‖ := by congr 1; abel
      _ = ‖f (z + v) - f z - f' (z + v - z)‖ := by
        simp only [v, ContinuousLinearMap.NonlinearRightInverse.right_inv, add_sub_cancel_left,
          sub_add_cancel]
      _ ≤ c * ‖z + v - z‖ := hf _ (hε hgz) _ (hε hz)
      _ ≤ c * (f'symm.nnnorm * dist (f z) y) := by
        gcongr
        simpa [dist_eq_norm'] using f'symm.bound (y - f z)
      _ = c * f'symm.nnnorm * dist (f z) y := by ring

Premises used: HMul.hMul, HSub.hSub, ContinuousLinearMap.NonlinearRightInverse.nnnorm, HAdd.hAdd, Dist.dist, DFunLike.coe, NNReal.toReal
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
⊢ ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) * dist (f z) y

Tactic:
have B :
    ∀ z ∈ closedBall b ε,
      g z ∈ closedBall b ε → dist (f (g z)) y ≤ c * f'symm.nnnorm * dist (f z) y := by
    intro z hz hgz
    set v := f'symm (y - f z)
    calc
      dist (f (g z)) y = ‖f (z + v) - y‖ := by rw [dist_eq_norm]
      _ = ‖f (z + v) - f z - f' v + f' v - (y - f z)‖ := by congr 1; abel
      _ = ‖f (z + v) - f z - f' (z + v - z)‖ := by
        simp only [v, ContinuousLinearMap.NonlinearRightInverse.right_inv, add_sub_cancel_left,
          sub_add_cancel]
      _ ≤ c * ‖z + v - z‖ := hf _ (hε hgz) _ (hε hz)
      _ ≤ c * (f'symm.nnnorm * dist (f z) y) := by
        gcongr
        simpa [dist_eq_norm'] using f'symm.bound (y - f z)
      _ = c * f'symm.nnnorm * dist (f z) y := by ring
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
apply :
  (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y ≤
    ε
⊢ w ∈ closedBall b ε

Tactic:
apply hw.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
rw :
  (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) * dist (f b) y ≤
    ε * (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ))
rw₁ : 0 < 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)
⊢ (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y ≤
    ε

Tactic:
rw [div_mul_eq_mul_div, div_le_iff₀]

Premises used: div_le_iff₀, div_mul_eq_mul_div
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
linarith : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ :
  1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≤ 0 →
    (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) - 1 + (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) - 0) = 0
⊢ 0 < 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑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) * dist (f b) y =
    (↑f'symm.nnnorm : ℝ) * dist (f b) y * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n)

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
hbc : 1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n ≤ 1
⊢ (↑f'symm.nnnorm : ℝ) * dist (f b) y * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) ≤
    (↑f'symm.nnnorm : ℝ) * dist (f b) y * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
hbc : 0 ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n
⊢ 1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n ≤ 1

Tactic:
rw [sub_le_self_iff]

Premises used: sub_le_self_iff
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
⊢ 0 ≤ ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
rw : (↑f'symm.nnnorm : ℝ) * dist (f b) y ≤ (↑f'symm.nnnorm : ℝ) * (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)
⊢ (↑f'symm.nnnorm : ℝ) * dist (f b) y * 1 ≤ (↑f'symm.nnnorm : ℝ) * (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
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
n : ℕ
w : E
hw :
  dist w b ≤
    (↑f'symm.nnnorm : ℝ) * (1 - ((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n) / (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) *
      dist (f b) y
hbc : dist (f b) y ≤ ((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε
⊢ (↑f'symm.nnnorm : ℝ) * dist (f b) y ≤ (↑f'symm.nnnorm : ℝ) * (((↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ)) * ε)

Tactic:
gcongr