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
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 : ℝ) * (((↑c : ℝ) * (↑f'symm.nnnorm : ℝ)) ^ n * dist (f b) y) =
    (↑f'symm.nnnorm : ℝ) * dist (f b) y * ((↑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.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₂ :
  (↑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
⊢ Dist.dist (u n) (u (n + 1)) ≤ (↑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

Premises used: HMul.hMul, ContinuousLinearMap.NonlinearRightInverse.nnnorm, HPow.hPow, HAdd.hAdd, Dist.dist, OfNat.ofNat, 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
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

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
-- 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
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), Tendsto u atTop (𝓝 x)

Tactic:
cauchySeq_tendsto_of_complete this

Premises used: cauchySeq_tendsto_of_complete
-- 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
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
inr : ∀ (x : E) (hx : Tendsto u atTop (𝓝 x)), y ∈ f '' closedBall b ε
⊢ y ∈ f '' closedBall b ε

Tactic:
obtain ⟨x, hx⟩ : ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete this

Premises used: cauchySeq_tendsto_of_complete
-- 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
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)
⊢ 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)
-- 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
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)
xmem : x ∈ closedBall b ε
⊢ y ∈ f '' closedBall b ε

Tactic:
⟨x, xmem, ?_⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- 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
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)
xmem : x ∈ closedBall b ε
inr : f x = y
⊢ y ∈ f '' closedBall b ε

Tactic:
refine ⟨x, xmem, ?_⟩
-- 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
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)
xmem : x ∈ closedBall b ε
simp : ∀ᶠ (a : ℕ) in atTop, u a ∈ closedBall b ε
⊢ Tendsto u atTop (𝓝[closedBall b ε] x)

Tactic:
simp only [nhdsWithin, tendsto_inf, hx, true_and, tendsto_principal]

Premises used: Filter.tendsto_inf, nhdsWithin, Filter.tendsto_principal, true_and
-- 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
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)
xmem : x ∈ closedBall b ε
⊢ ∀ᶠ (a : ℕ) in atTop, u a ∈ closedBall b ε

Tactic:
Eventually.of_forall fun n => C n _ (D n).2

Premises used: Filter.Eventually.of_forall, And.right
-- 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
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)
xmem : x ∈ closedBall b ε
⊢ ∀ᶠ (a : ℕ) in atTop, u a ∈ closedBall b ε

Tactic:
exact Eventually.of_forall fun n => C n _ (D n).2

Premises used: Filter.Eventually.of_forall, And.right
-- 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
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)
xmem : x ∈ closedBall b ε
⊢ Tendsto u atTop (𝓝[closedBall b ε] x)

Tactic:
have hx' : Tendsto u atTop (𝓝[closedBall b ε] x) := by
    simp only [nhdsWithin, tendsto_inf, hx, true_and, tendsto_principal]
    exact Eventually.of_forall fun n => C n _ (D n).2
-- 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
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)
xmem : x ∈ closedBall b ε
hx' : Tendsto u atTop (𝓝[closedBall b ε] x)
⊢ Tendsto (f ∘ u) atTop (𝓝 (f x))

Tactic:
have T1 : Tendsto (f ∘ u) atTop (𝓝 (f x)) :=
    (hf.continuousOn.mono hε x xmem).tendsto.comp hx'