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
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)
⊢ ∀ (x : ℝ), p x → ∀ y ∈ closedBall (f 0) x, (fun (y : F) ↦ ∃ (a : E), f a = y) y

Tactic:
fun R h y hy => h hy

Premises used: Set.Mem, setOf, Set.range
-- 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
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)
⊢ ∀ (x : ℝ), p x → ∀ y ∈ closedBall (f 0) x, (fun (y : F) ↦ ∃ (a : E), f a = y) y

Tactic:
exact fun R h y hy => h hy
-- 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' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
apply :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((f '' s).restrict (π := fun (a : F) ↦ E) (↑(hf.toPartialEquiv (s := s) hc).symm : F → E))
⊢ ContinuousOn (↑(hf.toPartialEquiv (s := s) hc).symm : F → E) (f '' s)

Tactic:
apply continuousOn_iff_continuous_restrict.2

Premises used: Iff.mpr, continuousOn_iff_continuous_restrict
-- 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' : 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))

Tactic:
((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous

Premises used: PartialEquiv.right_inv', Function.invFunOn, Set.Mem, setOf, dite, ApproximatesLinearOn.toPartialEquiv, ApproximatesLinearOn.antilipschitz, AntilipschitzWith.to_rightInvOn', LipschitzWith.continuous, 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
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)‖₊⁻¹
refine : MapsTo (hf.toPartialEquiv (s := s) hc).invFun (hf.toPartialEquiv (s := s) hc).target s
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((f '' s).restrict (π := fun (a : F) ↦ E) (↑(hf.toPartialEquiv (s := s) hc).symm : F → E))

Tactic:
refine ((hf.antilipschitz hc).to_rightInvOn' ?_ (hf.toPartialEquiv hc).right_inv').continuous

Premises used: PartialEquiv.right_inv', ApproximatesLinearOn.toPartialEquiv, ApproximatesLinearOn.antilipschitz, AntilipschitzWith.to_rightInvOn', LipschitzWith.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
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)‖₊⁻¹
⊢ MapsTo (hf.toPartialEquiv (s := s) hc).invFun (hf.toPartialEquiv (s := s) hc).target s

Tactic:
fun x hx => (hf.toPartialEquiv hc).map_target hx

Premises used: PartialEquiv.map_target, Function.invFunOn, Set.Mem, dite, ApproximatesLinearOn.toPartialEquiv, Set.MapsTo
-- 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' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ MapsTo (hf.toPartialEquiv (s := s) hc).invFun (hf.toPartialEquiv (s := s) hc).target s

Tactic:
exact fun x hx => (hf.toPartialEquiv hc).map_target hx

Premises used: PartialEquiv.map_target, ApproximatesLinearOn.toPartialEquiv
-- 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' : 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
set :
  let A := 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‖
⊢ ‖HSub.hSub (β := E)
        ((↑(hf.toPartialEquiv (s := s) hc).symm : F → E) x - (↑(hf.toPartialEquiv (s := s) hc).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‖

Tactic:
set A := hf.toPartialEquiv hc

Premises used: ApproximatesLinearOn.toPartialEquiv
-- 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' : 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
⊢ ∀ (z : E), (↑A : E → F) z = f z

Tactic:
have Af : ∀ z, A z = f z := fun z => rfl
-- 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' : 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
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‖
⊢ ‖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‖

Tactic:
rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- 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' : 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
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'‖
⊢ ‖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 hy with ⟨y', y's, rfl⟩

Premises used: Set.mem_image, Iff.mp, rfl
-- 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' : 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
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'‖
⊢ ‖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:
rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]

Premises used: PartialEquiv.left_inv
-- 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' : 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 : (a : F) → E) ((↑A : E → F) x' - (↑A : E → F) y') : E)‖ ≤
    (↑‖(↑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)

Tactic:
(f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearMap.bound_of_antilipschitz, ContinuousLinearEquiv.toContinuousLinearMap
-- 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' : 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
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)
⊢ (↑‖(↑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:
congr 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
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
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)
⊢ (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:
simp only [ContinuousLinearEquiv.apply_symm_apply, map_sub]

Premises used: map_sub, ContinuousLinearEquiv.apply_symm_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
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 (α := 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:
abel
-- 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' : 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
hbc : ‖HSub.hSub (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤ (↑c : ℝ) * ‖y' - x'‖
⊢ (↑‖(↑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:
gcongr
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
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 (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤ (↑c : ℝ) * ‖y' - x'‖

Tactic:
hf _ y's _ x's
-- 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' : 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 (β := F) ((↑A : E → F) y' - (↑A : E → F) x') ((f' : (a : E) → F) (y' - x') : F)‖ ≤ (↑c : ℝ) * ‖y' - x'‖

Tactic:
exact hf _ y's _ x's
-- 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' : 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
hbc : ‖y' - x'‖ ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖
⊢ (↑‖(↑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'‖))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
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
hbc : dist y' x' ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * dist ((↑A : E → F) y') ((↑A : E → F) x')
⊢ ‖y' - x'‖ ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) x'‖

Tactic:
rw [← dist_eq_norm, ← 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
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
⊢ dist y' x' ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * dist ((↑A : E → F) y') ((↑A : E → F) x')

Tactic:
(hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩

Premises used: AntilipschitzWith.le_mul_dist, Subtype.mk, ApproximatesLinearOn.antilipschitz, Set.restrict
-- 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' : 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
⊢ dist y' x' ≤ (↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * dist ((↑A : E → F) y') ((↑A : E → F) x')

Tactic:
exact (hf.antilipschitz hc).le_mul_dist ⟨y', y's⟩ ⟨x', x's⟩

Premises used: AntilipschitzWith.le_mul_dist, Subtype.mk, ApproximatesLinearOn.antilipschitz
-- 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' : 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
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'‖
⊢ (↑‖(↑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'‖

Tactic:
simp only [norm_sub_rev, NNReal.coe_mul]

Premises used: NNReal.coe_mul, norm_sub_rev
-- 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' : 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) 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:
ring