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
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'‖)
⊢ ‖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)‖₊ : ℝ) * ((↑c : ℝ) * ‖y' - x'‖) ≤
  (↑‖(↑f'.symm : F →L[𝕜] E)‖₊ : ℝ) *
    ((↑c : ℝ) * ((↑(‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ - c)⁻¹ : ℝ) * ‖(↑A : E → F) y' - (↑A : E → F) 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
-- 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)‖
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'‖))
⊢ ‖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)‖₊ : ℝ) *
    ((↑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: 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
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
⊢ Subsingleton F ∨ c < f'.toNonlinearRightInverse.nnnorm⁻¹
have rwa : ∀ (hc : Subsingleton F ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹)
  (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  Subsingleton F ∨ c < f'.toNonlinearRightInverse.nnnorm⁻¹
Tactic: rwa [f'.toEquiv.subsingleton_congr] at hc
Cleared hypotheses: hs
-- 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
inst_5 : CompleteSpace E
hf : ApproximatesLinearOn f (↑f' : E →L[𝕜] F) univ c
hc : Subsingleton E ∨ c < ‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹
⊢ E ≃ₜ F
have _ : (toOpenPartialHomeomorph f univ hf hc sorry).target = univ
Tactic: refine
    (hf.toOpenPartialHomeomorph _ _ hc isOpen_univ).toHomeomorphOfSourceEqUnivTargetEqUniv 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
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
have rw : Surjective f
Tactic: rw [toOpenPartialHomeomorph_target, image_univ, range_eq_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff (hypothesis)
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
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)
have this : hf.localInverse hf' hn (f a) = a
Tactic: have := hf.localInverse_apply_image hf' hn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff (goal)
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 (hf.localInverse hf' hn) (f a)
have hf₀' : HasFDerivAt (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F) (↑f' : E →L[𝕂] F)
  ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))
Tactic: apply (hf.toOpenPartialHomeomorph f hf' hn).contDiffAt_symm
    (image_mem_toOpenPartialHomeomorph_target hf hf' hn)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff (goal)
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))
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)
have hf₁ : ContDiffAt 𝕂 n (↑(toOpenPartialHomeomorph f hf hf' hn) : E → F)
  ((↑(toOpenPartialHomeomorph f hf hf' hn).symm : F → E) (f a))
Tactic: apply (hf.toOpenPartialHomeomorph f hf' hn).contDiffAt_symm
    (image_mem_toOpenPartialHomeomorph_target hf hf' hn)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : Subsingleton E ∨ 0 < c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have inl : ∀ (hE : Subsingleton E), ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
Tactic: rcases hc with hE | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have inr : ∀ (hc : 0 < c), ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
Tactic: rcases hc with hE | hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hE : Subsingleton E
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have 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‖
Tactic: refine ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
a : E
hf : HasStrictFDerivAt f f' a
c : ℝ≥0
hc : 0 < c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have 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‖
Tactic: have := hf.isLittleO.def hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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‖
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have 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‖}
Tactic: rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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‖}
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
have 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
Tactic: rcases this with ⟨s, has, hs⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
⊢ map f (𝓝 a) = 𝓝 (f a)
have hc : let c := f'symm.nnnorm⁻¹ / 2;
c = f'symm.nnnorm⁻¹ / 2
Tactic: set c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2 with hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
⊢ map f (𝓝 a) = 𝓝 (f a)
have f'symm_pos : 0 < f'symm.nnnorm
Tactic: have f'symm_pos : 0 < f'symm.nnnorm := f'.nonlinearRightInverseOfSurjective_nnnorm_pos h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
⊢ map f (𝓝 a) = 𝓝 (f a)
have cpos : 0 < c
Tactic: have cpos : 0 < c := by simp [hc, inv_pos, f'symm_pos]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
⊢ map f (𝓝 a) = 𝓝 (f a)
have obtain : ∀ (s : Set E) (s_nhds : s ∈ 𝓝 a) (hs : ApproximatesLinearOn f f' s c), map f (𝓝 a) = 𝓝 (f a)
Tactic: obtain ⟨s, s_nhds, hs⟩ : ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c :=
    hf.approximates_deriv_on_nhds (Or.inr cpos)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
s : Set E
s_nhds : s ∈ 𝓝 a
hs : ApproximatesLinearOn f f' s c
⊢ map f (𝓝 a) = 𝓝 (f a)
have apply : f'symm.nnnorm⁻¹ ≠ 0
Tactic: apply hs.map_nhds_eq f'symm s_nhds (Or.inr (NNReal.half_lt_self _))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
a : E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ ∃ (s : Set E),
    a ∈ s ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧
        ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
have simp : ∃ (s : Set E),
  (a ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ∧
    ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
Tactic: simp only [← and_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv (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
a : E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ ∃ (s : Set E),
    (a ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ∧
      ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
have refine : ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
Tactic: refine ((nhds_basis_opens a).exists_iff fun s t => ApproximatesLinearOn.mono_set).1 ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s
have obtain : ∀ (u : E → F) (hu : LipschitzWith (lipschitzExtensionConstant F * c) u) (uf : EqOn (f - (⇑f' : (a : E) → F)) u s),
  ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s
Tactic: obtain ⟨u, hu, uf⟩ :
    ∃ u : E → F, LipschitzWith (lipschitzExtensionConstant F * c) u ∧ EqOn (f - ⇑f') u s :=
    hf.lipschitzOnWith.extend_finite_dimension
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
x : E
hx : x ∈ s
simp_rw : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
⊢ f x = g x
have simp_rw₁ : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x)
Tactic: simp_rw [g, ← uf hx, Pi.sub_apply, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
x : E
hx : x ∈ s
simp_rw : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
simp_rw₁ : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x)
⊢ f x = g x
have simp_rw₂ : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (HSub.hSub (β := F) (f x) ((f' : (a : E) → F) x : F))
Tactic: simp_rw [g, ← uf hx, Pi.sub_apply, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
⊢ ∃ (g : E ≃ₜ F), EqOn f (⇑g : (a : E) → F) s
have fg : EqOn f g s
Tactic: have fg : EqOn f g s := fun x hx => by simp_rw [g, ← uf hx, Pi.sub_apply, add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
⊢ ApproximatesLinearOn g (↑f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c)
have a : LipschitzOnWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F)) univ
Tactic: apply LipschitzOnWith.approximatesLinearOn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f' : E →L[ℝ] F) s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖(↑f'.symm : F →L[ℝ] E)‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - (⇑f' : (a : E) → F)) u s
g : E → F := fun (x : E) ↦ HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (u x)
fg : EqOn f g s
⊢ LipschitzOnWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F)) univ
have a : LipschitzWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F))
Tactic: rw [lipschitzOnWith_univ]