awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ Surjective f
have apply : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y
Tactic: apply forall_of_forall_mem_closedBall (fun y : F => ∃ a, f a = y) (f 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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
have rw : (↑c : ℝ) < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ)
Tactic: rw [sub_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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y
have hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
Tactic: have hc' : (0 : ℝ) < N⁻¹ - c := by rw [sub_pos]; exact hc
-- 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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
⊢ ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
have hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
Tactic: have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 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
f' : E ≃L[𝕜] F
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
⊢ ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
have refine : ∀ (r : ℝ) (hr : 0 ≤ r), closedBall (f 0) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r) ⊆ f '' closedBall 0 r
Tactic: refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
-- 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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hr_1 : ∀ᶠ (r : ℝ) in atTop, 0 ≤ r
r : ℝ
hr : 0 ≤ r
⊢ closedBall (f 0) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r) ⊆ f '' closedBall 0 r
have refine : Subset.{u_2} (α := Set E) (closedBall 0 r) univ
Tactic: refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
-- 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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y
have hp : ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
Tactic: have hp : ∀ᶠ r : ℝ in atTop, p ((N⁻¹ - c) * r) := by
      have hr : ∀ᶠ r : ℝ in atTop, 0 ≤ r := eventually_ge_atTop 0
      refine hr.mono fun r hr => Subset.trans ?_ (image_subset_range f (closedBall 0 r))
      refine hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse hr ?_
      exact subset_univ _
-- 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
c : ℝ≥0
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hc' : 0 < (↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)
p : ℝ → Prop := fun (R : ℝ) ↦ closedBall (f 0) R ⊆ range f
hp : ∀ᶠ (r : ℝ) in atTop, p (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * r)
⊢ ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall (f 0) R, (fun (y : F) ↦ ∃ (a : E), f a = y) y
have refine : ∀ (x : ℝ), p x → ∀ y ∈ closedBall (f 0) x, (fun (y : F) ↦ ∃ (a : E), f a = y) y
Tactic: refine ((tendsto_id.const_mul_atTop hc').frequently hp.frequently).mono ?_
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ ContinuousOn (↑(hf.toPartialEquiv (s := s) hc).symm : F → E) (f '' s)
have apply : Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  ((f '' s).restrict (π := fun (a : F) ↦ E) (↑(hf.toPartialEquiv (s := s) hc).symm : F → E))
Tactic: apply continuousOn_iff_continuous_restrict.2
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((f '' s).restrict (π := fun (a : F) ↦ E) (↑(hf.toPartialEquiv (s := s) hc).symm : F → E))
have refine : MapsTo (hf.toPartialEquiv (s := s) hc).invFun (hf.toPartialEquiv (s := s) hc).target s
Tactic: refine ((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
⊢ ‖HSub.hSub (β := E) ((↑A.symm : F → E) x - (↑A.symm : F → E) y)
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (x - y) : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖x - y‖
have Af : ∀ (z : E), (↑A : E → F) z = f z
Tactic: have Af : ∀ z, A z = f z := fun z => rfl
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
⊢ ‖HSub.hSub (β := E) ((↑A.symm : F → E) x - (↑A.symm : F → E) y)
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (x - y) : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖x - y‖
have rcases : ∀ (x' : E) (x's : x' ∈ s) (hx : f x' ∈ f '' s),
  ‖HSub.hSub (β := E) ((↑A.symm : F → E) (f x') - (↑A.symm : F → E) y)
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (f x' - y) : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖f x' - y‖
Tactic: rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩
Cleared hypotheses: x, hx
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
⊢ ‖HSub.hSub (β := E) ((↑A.symm : F → E) (f x') - (↑A.symm : F → E) y)
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (f x' - y) : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖f x' - y‖
have rcases : ∀ (y' : E) (y's : y' ∈ s) (hy : f y' ∈ f '' s),
  ‖HSub.hSub (β := E) ((↑A.symm : F → E) (f x') - (↑A.symm : F → E) (f y'))
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (f x' - f y') : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖f x' - f y'‖
Tactic: rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩
Cleared hypotheses: y, hy
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖HSub.hSub (β := E) ((↑A.symm : F → E) (f x') - (↑A.symm : F → E) (f y'))
        (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) (f x' - f y') : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖f x' - f y'‖
have rw : ‖HSub.hSub (β := E) (x' - y') (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)‖ ≤
  (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖(↑A : E → F) x' - (↑A : E → F) y'‖
Tactic: rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      norm.{u_3} (E := F)
        ((f' : (a : E) → F)
            (HSub.hSub (β := E) (x' - y') ((f'.symm : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)) :
          F) =
    (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖
have e_a : (f' : (a : E) → F) (HSub.hSub (β := E) (x' - y') ((f'.symm : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)) =
  HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)
Tactic: congr 2
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ (f' : (a : E) → F) (HSub.hSub (β := E) (x' - y') ((f'.symm : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)) =
    HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)
have e_a : HSub.hSub (α := F) (β := F) ((f' : (a : E) → F) x' : F) ((f' : (a : E) → F) y' : F) -
    ((↑A : E → F) x' - (↑A : E → F) y') =
  (↑A : E → F) y' - (↑A : E → F) x' -
    HSub.hSub (α := F) (β := F) ((f' : (a : E) → F) y' : F) ((f' : (a : E) → F) x' : F)
Tactic: simp only [ContinuousLinearEquiv.apply_symm_apply, map_sub]
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤
    (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) * ((↑c : ℝ) * ‖y' - x'‖)
have hbc : ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤ (↑c : ℝ) * ‖y' - x'‖
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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) * ((↑c : ℝ) * ‖y' - x'‖) ≤
    (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      ((↑c : ℝ) * ((↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖))
have hbc : ‖y' - x'‖ ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖
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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖y' - x'‖ ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖
have hbc : dist y' x' ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * dist ((↑A : E → F) y') ((↑A : E → F) x')
Tactic: rw [← dist_eq_norm, ← dist_eq_norm]
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      ((↑c : ℝ) * ((↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖)) =
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖(↑A : E → F) x' - (↑A : E → F) y'‖
have simp : (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
    ((↑c : ℝ) * ((↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) x' - (↑A : E → F) y'‖)) =
  (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) * (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * (↑c : ℝ) *
    ‖(↑A : E → F) x' - (↑A : E → F) y'‖
Tactic: simp only [norm_sub_rev, NNReal.coe_mul]
-- 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
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
⊢ ‖HSub.hSub (β := E) (x' - y') (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖(↑A : E → F) x' - (↑A : E → F) y'‖
have y'₁ : (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
    norm.{u_3} (E := F)
      ((f' : (a : E) → F)
          (HSub.hSub (β := E) (x' - y') ((f'.symm : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)) :
        F) =
  (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
    ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖
Tactic: calc
    ‖x' - y' - f'.symm (A x' - A y')‖ ≤ N * ‖f' (x' - y' - f'.symm (A x' - A y'))‖ :=
      (f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _
    _ = N * ‖A y' - A x' - f' (y' - x')‖ := by
      congr 2
      simp only [ContinuousLinearEquiv.apply_symm_apply, map_sub]
      abel
    _ ≤ N * (c * ‖y' - x'‖) := by gcongr; exact hf _ y's _ x's
    _ ≤ N * (c * (((N⁻¹ - c)⁻¹ : ℝ≥0) * ‖A y' - A x'‖)) := by
      gcongr
      rw [← dist_eq_norm, ← dist_eq_norm]
      exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
    _ = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ‖A x' - A y'‖ := by
      simp only [norm_sub_rev, NNReal.coe_mul]; ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
A : PartialEquiv E F := hf.toPartialEquiv (s := s) hc
Af : ∀ (z : E), (↑A : E → F) z = f z
x' : E
x's : x' ∈ s
hx : f x' ∈ f '' s
y' : E
y's : y' ∈ s
hy : f y' ∈ f '' s
y'₁ :
  (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      norm.{u_3} (E := F)
        ((f' : (a : E) → F)
            (HSub.hSub (β := E) (x' - y') ((f'.symm : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)) :
          F) =
    (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
      ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖
⊢ ‖HSub.hSub (β := E) (x' - y') (((↑f'.symm : F →L[𝕜] E) : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)‖ ≤
    (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊ * (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ * c) : ℝ) * ‖(↑A : E → F) x' - (↑A : E → F) y'‖
have y'₂ : (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
    ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤
  (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) * ((↑c : ℝ) * ‖y' - x'‖)
Tactic: calc
    ‖x' - y' - f'.symm (A x' - A y')‖ ≤ N * ‖f' (x' - y' - f'.symm (A x' - A y'))‖ :=
      (f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _
    _ = N * ‖A y' - A x' - f' (y' - x')‖ := by
      congr 2
      simp only [ContinuousLinearEquiv.apply_symm_apply, map_sub]
      abel
    _ ≤ N * (c * ‖y' - x'‖) := by gcongr; exact hf _ y's _ x's
    _ ≤ N * (c * (((N⁻¹ - c)⁻¹ : ℝ≥0) * ‖A y' - A x'‖)) := by
      gcongr
      rw [← dist_eq_norm, ← dist_eq_norm]
      exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩
    _ = (N * (N⁻¹ - c)⁻¹ * c : ℝ≥0) * ‖A x' - A y'‖ := by
      simp only [norm_sub_rev, NNReal.coe_mul]; ring