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
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f f' s c
⊢ ContinuousOn f s

Tactic:
continuousOn_iff_continuous_restrict.2 hf.continuous

Premises used: Iff.mpr, continuousOn_iff_continuous_restrict, ApproximatesLinearOn.continuous
-- 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 : ℝ)) * ε)
inl : ∀ (hc : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)), y ∈ f '' closedBall b ε
inr : ∀ (hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹), y ∈ f '' closedBall b ε
⊢ y ∈ f '' closedBall b ε

Tactic:
rcases le_or_gt (f'symm.nnnorm : ℝ)⁻¹ c with hc | hc

Premises used: ContinuousLinearMap.NonlinearRightInverse.nnnorm, le_or_gt, Inv.inv, 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
⊢ b ∈ closedBall b ε

Tactic:
simp [ε0]
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
inl : f b = y
⊢ y ∈ f '' closedBall b ε

Tactic:
refine ⟨b, by simp [ε0], ?_⟩
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
linarith :
  0 < (↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ) →
    1 * (↑f'symm.nnnorm : ℝ)⁻¹ - 1 * (↑c : ℝ) + (HMul.hMul (α := ℝ) 1 0 - (1 * (↑f'symm.nnnorm : ℝ)⁻¹ - 1 * (↑c : ℝ))) =
      0
⊢ (↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ) ≤ 0

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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
⊢ dist y (f b) ≤ 0

Tactic:
have : dist y (f b) ≤ 0 :=
      (mem_closedBall.1 hy).trans (mul_nonpos_of_nonpos_of_nonneg (by linarith) ε0)
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
this : dist y (f b) ≤ 0
⊢ y = f b

Tactic:
simp only [dist_le_zero] at this

Premises used: dist_le_zero
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
this : y = f b
inl inl₁ : f b = f b
⊢ f b = y

Tactic:
rw [this]
-- 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 : ℝ)⁻¹
rw : 0 < (↑f'symm.nnnorm : ℝ)⁻¹
⊢ 0 < (↑f'symm.nnnorm : ℝ)

Tactic:
rw [← inv_pos]

Premises used: inv_pos
-- 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 : ℝ)⁻¹
⊢ 0 < (↑f'symm.nnnorm : ℝ)⁻¹

Tactic:
(NNReal.coe_nonneg _).trans_lt hc

Premises used: NNReal.coe_nonneg, LE.le.trans_lt
-- 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 : ℝ)⁻¹
⊢ 0 < (↑f'symm.nnnorm : ℝ)⁻¹

Tactic:
exact (NNReal.coe_nonneg _).trans_lt hc

Premises used: NNReal.coe_nonneg, LE.le.trans_lt
-- 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 : ℝ)⁻¹
⊢ 0 < (↑f'symm.nnnorm : ℝ)

Tactic:
have If' : (0 : ℝ) < f'symm.nnnorm := by rw [← inv_pos]; exact (NNReal.coe_nonneg _).trans_lt hc
-- 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 : ℝ)
rwa : ∀ (hc : (↑c : ℝ) < 1 / (↑f'symm.nnnorm : ℝ)) (If' : 0 < (↑f'symm.nnnorm : ℝ)), (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hc : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1) (If' : 0 < (↑f'symm.nnnorm : ℝ)), (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1

Tactic:
rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc

Premises used: lt_div_iff₀, inv_eq_one_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 : ℝ)
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1

Tactic:
have Icf' : (c : ℝ) * f'symm.nnnorm < 1 := by rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc
-- 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
h : 0 < 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)
⊢ 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- 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
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
⊢ 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0

Tactic:
have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt; 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
⊢ let g : (x : E) → E := fun (x : E) ↦ x + f'symm.toFun (y - f x);
  g = fun (x : E) ↦ x + f'symm.toFun (y - f x)

Tactic:
set g := fun x => x + f'symm (y - f x) with hg

Premises used: HSub.hSub, HAdd.hAdd, ContinuousLinearMap.NonlinearRightInverse.toFun
-- 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)
⊢ let u : (n : ℕ) → E := fun (n : ℕ) ↦ g^[n] b;
  u = fun (n : ℕ) ↦ g^[n] b

Tactic:
set u := fun n : ℕ => g^[n] b with hu

Premises used: Nat.iterate
-- 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
⊢ ∀ (n : ℕ), u (n + 1) = g (u n)

Tactic:
simp [hu, ← iterate_succ_apply' g _ b]

Premises used: Function.iterate_succ_apply'
-- 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
⊢ ∀ (n : ℕ), u (n + 1) = g (u n)

Tactic:
have usucc : ∀ n, u (n + 1) = g (u n) := by simp [hu, ← iterate_succ_apply' g _ b]
-- 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)
z : E
rw : ‖f'symm.toFun (y - f z)‖ ≤ (↑f'symm.nnnorm : ℝ) * ‖y - f z‖
⊢ dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y

Tactic:
rw [dist_eq_norm, hg, add_sub_cancel_left, dist_eq_norm']

Premises used: dist_eq_norm, add_sub_cancel_left, dist_eq_norm'
-- 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)
z : E
⊢ ‖f'symm.toFun (y - f z)‖ ≤ (↑f'symm.nnnorm : ℝ) * ‖y - f z‖

Tactic:
f'symm.bound _

Premises used: 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)
z : E
⊢ ‖f'symm.toFun (y - f z)‖ ≤ (↑f'symm.nnnorm : ℝ) * ‖y - f z‖

Tactic:
exact f'symm.bound _

Premises used: 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)
⊢ ∀ (z : E), dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y

Tactic:
have A : ∀ z, dist (g z) z ≤ f'symm.nnnorm * dist (f z) y := by
    intro z
    rw [dist_eq_norm, hg, add_sub_cancel_left, dist_eq_norm']
    exact f'symm.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)
rw rw₁ : ‖f (g z) - y‖ = ‖f (z + v) - y‖
⊢ dist (f (g z)) y = ‖f (z + v) - y‖

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- 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)
e_a :
  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)
⊢ ‖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)‖

Tactic:
congr 1
-- 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)
⊢ 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)

Tactic:
abel