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' : 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)‖
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'‖)
y'₃ :
  (↑‖(↑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'‖))
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'‖
⊢ ‖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:
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

Premises used: ContinuousLinearEquiv.antilipschitz, Norm.norm, ContinuousLinearEquiv.symm, HMul.hMul, HSub.hSub, PartialEquiv.toFun, DFunLike.coe, NNReal.toReal, 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hc : Subsingleton F ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹)
    (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    Subsingleton F ∨ c < f'.toNonlinearRightInverse.nnnorm⁻¹
⊢ Subsingleton F ∨ c < f'.toNonlinearRightInverse.nnnorm⁻¹

Tactic:
rwa [f'.toEquiv.subsingleton_congr] at hc

Premises used: ContinuousLinearEquiv.toLinearEquiv, Equiv.subsingleton_congr, LinearEquiv.toEquiv
-- 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (↑(toOpenPartialHomeomorph f s hf hc hs) : E → F) = f

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (toOpenPartialHomeomorph f s hf hc hs).source = s

Tactic:
rfl

Premises used: 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (toOpenPartialHomeomorph f s hf hc hs).target = f '' s

Tactic:
rfl

Premises used: setOf, Set.image, 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
_ : (toOpenPartialHomeomorph f univ hf hc ⋯).target = univ
⊢ E ≃ₜ F

Tactic:
refine
    (hf.toOpenPartialHomeomorph _ _ hc isOpen_univ).toHomeomorphOfSourceEqUnivTargetEqUniv rfl ?_

Premises used: isOpen_univ, ApproximatesLinearOn.toOpenPartialHomeomorph, OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv, 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
rw : Surjective f
⊢ (toOpenPartialHomeomorph f univ hf hc ⋯).target = univ

Tactic:
rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]

Premises used: Set.range_eq_univ, Set.image_univ, ApproximatesLinearOn.toOpenPartialHomeomorph_target
-- 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ Surjective f

Tactic:
hf.surjective hc

Premises used: ApproximatesLinearOn.surjective
-- 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ Surjective f

Tactic:
exact hf.surjective hc

Premises used: ApproximatesLinearOn.surjective
-- 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
⊢ closedBall (f b) (((↑‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ : ℝ) - (↑c : ℝ)) * ε) ⊆ (toOpenPartialHomeomorph f s hf hc hs).target

Tactic:
(hf.surjOn_closedBall_of_nonlinearRightInverse f'.toNonlinearRightInverse ε0 hε).mono hε
    Subset.rfl

Premises used: ContinuousLinearEquiv.toNonlinearRightInverse, ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverse, Set.SurjOn.mono, setOf, Set.SurjOn, Set.Subset.rfl, Set.image
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
⊢ (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F) = f

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
⊢ a ∈ (toOpenPartialHomeomorph f hf hf' hn).source

Tactic:
(hf.hasStrictFDerivAt' hf' hn).mem_toOpenPartialHomeomorph_source

Premises used: Set.Mem, HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, ContDiffAt.hasStrictFDerivAt'
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
⊢ f a ∈ (toOpenPartialHomeomorph f hf hf' hn).target

Tactic:
(hf.hasStrictFDerivAt' hf' hn).image_mem_toOpenPartialHomeomorph_target

Premises used: Set.Mem, ContDiffAt.hasStrictFDerivAt', HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
⊢ hf.localInverse hf' hn (f a) = a

Tactic:
(hf.hasStrictFDerivAt' hf' hn).localInverse_apply_image

Premises used: HasStrictFDerivAt.localInverse_apply_image, ContDiffAt.hasStrictFDerivAt', ContDiffAt.localInverse
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
⊢ hf.localInverse hf' hn (f a) = a

Tactic:
have := hf.localInverse_apply_image hf' hn
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
hf₀' :
  HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F) (↑f' : E →L[𝕂] F)
    ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))
hf₁ :
  ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F)
    ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))
apply : E ≃L[𝕂] F
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

Tactic:
apply (hf.toOpenPartialHomeomorph f hf' hn).contDiffAt_symm
    (image_mem_toOpenPartialHomeomorph_target hf hf' hn)

Premises used: ContDiffAt.image_mem_toOpenPartialHomeomorph_target, OpenPartialHomeomorph.contDiffAt_symm, ContDiffAt.toOpenPartialHomeomorph
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a

Tactic:
hf'
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F) (↑f' : E →L[𝕂] F)
    ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))

Tactic:
convert! hf'
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n f a

Tactic:
hf
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
Goal:
𝕂 : Type u_1
inst : RCLike 𝕂
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕂 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕂 F
inst_5 : CompleteSpace E
f : E → F
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕂) f (↑f' : E →L[𝕂] F) a
hn : n ≠ 0
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F)
    ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))

Tactic:
convert! hf
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
f' a : 𝕜
hf : HasStrictDerivAt f f' a
hf' : f' ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 a, localInverse f f' a hf hf' (f x) = x

Tactic:
HasStrictFDerivAt.eventually_left_inverse ..

Premises used: HasStrictFDerivAt.eventually_left_inverse
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
f' a : 𝕜
hf : HasStrictDerivAt f f' a
hf' : f' ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 (f a), f (localInverse f f' a hf hf' x) = x

Tactic:
HasStrictFDerivAt.eventually_right_inverse ..

Premises used: HasStrictFDerivAt.eventually_right_inverse
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
f' a : 𝕜
hf : HasStrictDerivAt f f' a
hf' : f' ≠ 0
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
(hf.hasStrictFDerivAt_equiv hf').map_nhds_eq_of_equiv

Premises used: HasStrictFDerivAt.map_nhds_eq_of_equiv, HasStrictDerivAt.hasStrictFDerivAt_equiv
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
f' a : 𝕜
hf : HasStrictDerivAt f f' a
hf' : f' ≠ 0
⊢ HasStrictDerivAt (localInverse f f' a hf hf') f'⁻¹ (f a)

Tactic:
(hf.hasStrictFDerivAt_equiv hf').to_localInverse

Premises used: HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, HasStrictFDerivAt.to_localInverse, LinearMap.smulRight, HasStrictDerivAt, HasStrictDerivAt.hasStrictFDerivAt_equiv, LinearMap.toSpanSingleton, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f : 𝕜 → 𝕜
f' a : 𝕜
hf : HasStrictDerivAt f f' a
hf' : f' ≠ 0
g : 𝕜 → 𝕜
hg : ∀ᶠ (x : 𝕜) in 𝓝 a, g (f x) = x
⊢ HasStrictDerivAt g f'⁻¹ (f a)

Tactic:
(hf.hasStrictFDerivAt_equiv hf').to_local_left_inverse hg

Premises used: HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, LinearMap.smulRight, HasStrictFDerivAt.to_local_left_inverse, HasStrictDerivAt, HasStrictDerivAt.hasStrictFDerivAt_equiv, LinearMap.toSpanSingleton, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
f f' : 𝕜 → 𝕜
hf : ∀ (x : 𝕜), HasStrictDerivAt f (f' x) x
h0 : ∀ (x : 𝕜), f' x ≠ 0
⊢ IsOpenMap f

Tactic:
isOpenMap_iff_nhds_le.2 fun x => ((hf x).map_nhds_eq (h0 x)).ge

Premises used: Iff.mpr, Eq.ge, isOpenMap_iff_nhds_le, HasStrictDerivAt.map_nhds_eq
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : Subsingleton E ∨ 0 < c
inl : ∀ (hE : Subsingleton E), ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
inr : ∀ (hc : 0 < c), ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
rcases hc with hE | hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => ?_⟩

Premises used: trivial, Set.univ, isOpen_univ, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
inl :
  ∀ (x : E),
    Membership.mem (γ := Set E) univ x →
      ∀ (y : E),
        Membership.mem (γ := Set E) univ y →
          ‖HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F)‖ ≤ (↑c : ℝ) * ‖x - y‖
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
refine ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => ?_⟩
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
⊢ ‖HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F)‖ ≤ (↑c : ℝ) * ‖x - y‖

Tactic:
simp [@Subsingleton.elim E hE x y]

Premises used: Subsingleton.elim
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∀ᶠ (x : E × E) in 𝓝 (a, a),
    ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖

Tactic:
have := hf.isLittleO.def hc
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this :
  ∀ᶠ (x : E × E) in 𝓝 (a, a),
    ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖
⊢ ∃ t ∈ 𝓝 a,
    t ×ˢ t ⊆
      {x : E × E | ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖}

Tactic:
rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this

Premises used: Filter.Eventually, nhds_prod_eq, Filter.mem_prod_same_iff
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
this :
  ∃ t ∈ 𝓝 a,
    t ×ˢ t ⊆
      {x : E × E | ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖}
inr :
  ∀ (s : Set E) (has : s ∈ 𝓝 a)
    (hs :
      s ×ˢ s ⊆
        {x : E × E |
          ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖}),
    ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
rcases this with ⟨s, has, hs⟩
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
s : Set E
has : s ∈ 𝓝 a
hs :
  s ×ˢ s ⊆
    {x : E × E | ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖}
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩

Premises used: And.intro, Exists.intro, Set.mk_mem_prod
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
s : Set E
has : s ∈ 𝓝 a
hs :
  s ×ˢ s ⊆
    {x : E × E | ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ ≤ (↑c : ℝ) * ‖x.1 - x.2‖}
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
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
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
h : (↑f' : E →ₗ[𝕜] F).range = ⊤
f'symm : f'.NonlinearRightInverse := f'.nonlinearRightInverseOfSurjective h
⊢ let c := f'symm.nnnorm⁻¹ / 2;
  c = f'symm.nnnorm⁻¹ / 2

Tactic:
set c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2 with hc

Premises used: ContinuousLinearMap.NonlinearRightInverse.nnnorm