awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
have hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
Tactic: have hfd : HasStrictFDerivAt f i.toContinuousLinearMap x := hf.hasStrictDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
have hx : x ∈ R.source
Tactic: have hx : x ∈ R.source := HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)
have refine : Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
  (FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1)
  ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
      (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
    (↑i : 𝕜 →L[𝕜] 𝕜))
Tactic: refine R.hasFPowerSeriesAt_symm hx hf.hasFPowerSeriesAt (i := i) ?_ |>.analyticAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
    (FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
        (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
      (↑i : 𝕜 →L[𝕜] 𝕜))
have h : Eq (α := 𝕜)
  ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1 :
        (a : (i : Fin 1) → 𝕜) → 𝕜)
      fun (x : Fin 1) ↦ 1 :
    𝕜)
  ((((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
              (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
            (↑i : 𝕜 →L[𝕜] 𝕜) :
          ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜) :
        (a : (i : Fin 1) → 𝕜) → 𝕜)
      fun (x : Fin 1) ↦ 1 :
    𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)
have refine : ∀ (hg : AnalyticAt 𝕜 (g ∘ f) x), AnalyticAt 𝕜 g (f x)
Tactic: refine ⟨fun hg ↦ ?_, (AnalyticAt.comp · hf)⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
⊢ AnalyticAt 𝕜 g (f x)
have hra : AnalyticAt 𝕜 r (f x)
Tactic: have hra : AnalyticAt 𝕜 r (f x) := hf.analyticAt_localInverse hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
⊢ AnalyticAt 𝕜 g (f x)
have this : r (f x) = x
Tactic: have : r (f x) = x := HasStrictFDerivAt.localInverse_apply_image ..
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f x)
have hg₁ : AnalyticAt 𝕜 (g ∘ f) (r (f x))
Tactic: rw [← this] at hg
Cleared hypotheses: hg, hra, this
-- 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
f' : E →L[𝕜] F
s : Set E
c c' : ℝ≥0
hc : c ≤ c'
hf : ApproximatesLinearOn f f' s c
x : E
hx : x ∈ s
y : E
hy : y ∈ s
⊢ (↑c : ℝ) * ‖x - y‖ ≤ (↑c' : ℝ) * ‖x - y‖
have ha : 0 ≤ ‖x - 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
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F) =
    HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x - HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) y
have simp : f x - f y - HSub.hSub (α := F) (β := F) ((f' : (a : E) → F) x : F) ((f' : (a : E) → F) y : F) =
  HSub.hSub (β := F) (f x) ((f' : (a : E) → F) x : F) - HSub.hSub (β := F) (f y) ((f' : (a : E) → F) y : F)
Tactic: simp only [map_sub, Pi.sub_apply]
-- 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
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - (⇑f' : (a : E) → F)) s
have this : ∀ (x y : E),
  HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F) =
    HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x - HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) y
Tactic: have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y := fun x y ↦ by
    simp only [map_sub, Pi.sub_apply]; abel
-- 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 : ℝ)) * ε)
⊢ y ∈ f '' closedBall b ε
have inl : ∀ (hc : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)), y ∈ f '' closedBall b ε
Tactic: rcases le_or_gt (f'symm.nnnorm : ℝ)⁻¹ c with hc | hc
-- 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 : ℝ)) * ε)
inl : ∀ (hc : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)), y ∈ f '' closedBall b ε
⊢ y ∈ f '' closedBall b ε
have inr : ∀ (hc : (↑c : ℝ) < (↑f'symm.nnnorm : ℝ)⁻¹), y ∈ f '' closedBall b ε
Tactic: rcases le_or_gt (f'symm.nnnorm : ℝ)⁻¹ c with hc | hc
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
⊢ y ∈ f '' closedBall b ε
have inl : f b = y
Tactic: refine ⟨b, by simp [ε0], ?_⟩
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
⊢ (↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ) ≤ 0
have linarith : 0 < (↑f'symm.nnnorm : ℝ)⁻¹ - (↑c : ℝ) →
  1 * (↑f'symm.nnnorm : ℝ)⁻¹ - 1 * (↑c : ℝ) + (HMul.hMul (α := ℝ) 1 0 - (1 * (↑f'symm.nnnorm : ℝ)⁻¹ - 1 * (↑c : ℝ))) = 0
Tactic: linarith
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
⊢ f b = y
have this : 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)
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
this : dist y (f b) ≤ 0
⊢ f b = y
have this₁ : y = f b
Tactic: simp only [dist_le_zero] at this
Cleared hypotheses: this
-- 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 : (↑f'symm.nnnorm : ℝ)⁻¹ ≤ (↑c : ℝ)
this : y = f b
⊢ f b = y
have inl : f b = f b
Tactic: rw [this]
-- 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 : ℝ)⁻¹
⊢ 0 < (↑f'symm.nnnorm : ℝ)
have rw : 0 < (↑f'symm.nnnorm : ℝ)⁻¹
Tactic: rw [← inv_pos]
-- 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 : ℝ)⁻¹
⊢ y ∈ f '' closedBall b ε
have If' : 0 < (↑f'symm.nnnorm : ℝ)
Tactic: have If' : (0 : ℝ) < f'symm.nnnorm := by rw [← inv_pos]; exact (NNReal.coe_nonneg _).trans_lt hc
-- 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 : ℝ)
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
have rwa : ∀ (hc : (↑c : ℝ) < 1 / (↑f'symm.nnnorm : ℝ)) (If' : 0 < (↑f'symm.nnnorm : ℝ)), (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Tactic: rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc
Cleared hypotheses: hc, If'
-- 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 : ℝ)
rwa : ∀ (hc : (↑c : ℝ) < 1 / (↑f'symm.nnnorm : ℝ)) (If' : 0 < (↑f'symm.nnnorm : ℝ)), (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
⊢ (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
have rwa₁ : ∀ (hc : (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1) (If' : 0 < (↑f'symm.nnnorm : ℝ)), (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) < 1
Tactic: rwa [inv_eq_one_div, lt_div_iff₀ If'] at hc
Cleared hypotheses: hc, If'
-- 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 : ℝ)
⊢ y ∈ f '' closedBall b ε
have Icf' : (↑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
-- 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
⊢ 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
have h : 0 < 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)
Tactic: apply ne_of_gt
-- 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
⊢ 0 < 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ)
have linarith : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≤ 0 →
  (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) - 1 + (1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) - 0) = 0
Tactic: linarith
-- 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
⊢ y ∈ f '' closedBall b ε
have Jcf' : 1 - (↑c : ℝ) * (↑f'symm.nnnorm : ℝ) ≠ 0
Tactic: have Jcf' : (1 : ℝ) - c * f'symm.nnnorm ≠ 0 := by apply ne_of_gt; linarith
-- 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
⊢ y ∈ f '' closedBall b ε
have hg : 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
-- 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)
⊢ y ∈ f '' closedBall b ε
have hu : 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
-- 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
⊢ y ∈ f '' closedBall b ε
have usucc : ∀ (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]
-- 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)
z : E
⊢ dist (g z) z ≤ (↑f'symm.nnnorm : ℝ) * dist (f z) y
have rw : ‖f'symm.toFun (y - f z)‖ ≤ (↑f'symm.nnnorm : ℝ) * ‖y - f z‖
Tactic: rw [dist_eq_norm, hg, add_sub_cancel_left, dist_eq_norm']