awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
⊢ 0 < f'symm.nnnorm

Tactic:
have f'symm_pos : 0 < f'symm.nnnorm := f'.nonlinearRightInverseOfSurjective_nnnorm_pos h
-- 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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
⊢ 0 < c

Tactic:
simp [hc, inv_pos, f'symm_pos]

Premises used: inv_pos
-- 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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
⊢ 0 < c

Tactic:
have cpos : 0 < c := by simp [hc, inv_pos, f'symm_pos]
-- 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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c

Tactic:
hf.approximates_deriv_on_nhds (Or.inr cpos)

Premises used: HasStrictFDerivAt.approximates_deriv_on_nhds, Or.inr
-- 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
c : ℝ≥0 := f'symm.nnnorm⁻¹ / 2
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
obtain : ∀ (s : Set E) (s_nhds : s ∈ 𝓝 a) (hs : ApproximatesLinearOn f f' s c), map f (𝓝 a) = 𝓝 (f a)
⊢ 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)

Premises used: HasStrictFDerivAt.approximates_deriv_on_nhds, nhds, Or.inr
-- 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
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
apply : f'symm.nnnorm⁻¹ ≠ 0
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
apply hs.map_nhds_eq f'symm s_nhds (Or.inr (NNReal.half_lt_self _))

Premises used: NNReal.half_lt_self, ApproximatesLinearOn.map_nhds_eq, Or.inr
-- 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
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
⊢ f'symm.nnnorm⁻¹ ≠ 0

Tactic:
simp [ne_of_gt f'symm_pos]

Premises used: ne_of_gt
-- 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' : E →L[𝕜] F) a
simp :
  ∃ (s : Set E),
    (a ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ∧
      ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
⊢ ∃ (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]

Premises used: and_assoc
-- 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' : 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)

Tactic:
((nhds_basis_opens a).exists_iff fun s t => ApproximatesLinearOn.mono_set).1 ?_

Premises used: ApproximatesLinearOn.mono_set, Filter.HasBasis.exists_iff, Iff.mp, nhds_basis_opens
-- 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' : E →L[𝕜] F) a
refine : ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)
⊢ ∃ (s : Set E),
    (a ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ∧
      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 ?_

Premises used: ApproximatesLinearOn.mono_set, Filter.HasBasis.exists_iff, Iff.mp, nhds_basis_opens
-- 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' : E →L[𝕜] F) a
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)

Tactic:
hf.approximates_deriv_on_nhds <|
      f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'

Premises used: Iff.mpr, half_pos, HasStrictFDerivAt.approximates_deriv_on_nhds, id, inv_pos, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, Or.imp
-- 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' : E →L[𝕜] F) a
⊢ ∃ s ∈ 𝓝 a, ApproximatesLinearOn f (↑f' : E →L[𝕜] F) s (‖(↑f'.symm : F →L[𝕜] E)‖₊⁻¹ / 2)

Tactic:
exact
    hf.approximates_deriv_on_nhds <|
      f'.subsingleton_or_nnnorm_symm_pos.imp id fun hf' => half_pos <| inv_pos.2 hf'

Premises used: half_pos, HasStrictFDerivAt.approximates_deriv_on_nhds, id, ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos, Or.imp
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ (↑(toOpenPartialHomeomorph f hf) : E → F) = f

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ a ∈ (toOpenPartialHomeomorph f hf).source

Tactic:
(Classical.choose_spec hf.approximates_deriv_on_open_nhds).1

Premises used: Set.Mem, Classical.choose_spec, And.left, HasStrictFDerivAt.approximates_deriv_on_open_nhds, Classical.choose
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ f a ∈ (toOpenPartialHomeomorph f hf).target

Tactic:
(hf.toOpenPartialHomeomorph f).map_source hf.mem_toOpenPartialHomeomorph_source

Premises used: Set.Mem, HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.map_source, HasStrictFDerivAt.toOpenPartialHomeomorph
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ map f (𝓝 a) = 𝓝 (f a)

Tactic:
(hf.toOpenPartialHomeomorph f).map_nhds_eq hf.mem_toOpenPartialHomeomorph_source

Premises used: HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.toFun', HasStrictFDerivAt.toOpenPartialHomeomorph, OpenPartialHomeomorph.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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ localInverse f f' a hf = (↑(toOpenPartialHomeomorph f hf).symm : F → E)

Tactic:
rfl

Premises used: HasStrictFDerivAt.localInverse, rfl
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ ∀ᶠ (x : E) in 𝓝 a, localInverse f f' a hf (f x) = x

Tactic:
(hf.toOpenPartialHomeomorph f).eventually_left_inverse hf.mem_toOpenPartialHomeomorph_source

Premises used: HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.eventually_left_inverse, HasStrictFDerivAt.localInverse, OpenPartialHomeomorph.toFun', HasStrictFDerivAt.toOpenPartialHomeomorph
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ localInverse f f' a hf (f a) = a

Tactic:
hf.eventually_left_inverse.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds, HasStrictFDerivAt.eventually_left_inverse
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ ∀ᶠ (y : F) in 𝓝 (f a), f (localInverse f f' a hf y) = y

Tactic:
(hf.toOpenPartialHomeomorph f).eventually_right_inverse' hf.mem_toOpenPartialHomeomorph_source

Premises used: HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, HasStrictFDerivAt.localInverse, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.eventually_right_inverse', HasStrictFDerivAt.toOpenPartialHomeomorph
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ ContinuousAt (localInverse f f' a hf) (f a)

Tactic:
(hf.toOpenPartialHomeomorph f).continuousAt_symm hf.image_mem_toOpenPartialHomeomorph_target

Premises used: HasStrictFDerivAt.localInverse, HasStrictFDerivAt.toOpenPartialHomeomorph, OpenPartialHomeomorph.continuousAt_symm, HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ Tendsto (localInverse f f' a hf) (𝓝 (f a)) (𝓝 a)

Tactic:
(hf.toOpenPartialHomeomorph f).tendsto_symm hf.mem_toOpenPartialHomeomorph_source

Premises used: HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, HasStrictFDerivAt.localInverse, OpenPartialHomeomorph.toFun', HasStrictFDerivAt.toOpenPartialHomeomorph, OpenPartialHomeomorph.tendsto_symm
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
g : F → E
hg : ∀ᶠ (x : E) in 𝓝 a, g (f x) = x
⊢ ∀ᶠ (y : F) in 𝓝 (f a), g y = localInverse f f' a hf y

Tactic:
eventuallyEq_of_left_inv_of_right_inv hg hf.eventually_right_inverse <|
    (hf.toOpenPartialHomeomorph f).tendsto_symm hf.mem_toOpenPartialHomeomorph_source

Premises used: HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, Filter.EventuallyEq, Filter.eventuallyEq_of_left_inv_of_right_inv, HasStrictFDerivAt.eventually_right_inverse, HasStrictFDerivAt.toOpenPartialHomeomorph, OpenPartialHomeomorph.tendsto_symm
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
⊢ HasStrictFDerivAt (↑(toOpenPartialHomeomorph f hf) : E → F) (↑f' : E →L[𝕜] F)
    ((↑(toOpenPartialHomeomorph f hf).symm : F → E) (f a))

Tactic:
simpa [← localInverse_def] using hf

Premises used: HasStrictFDerivAt.localInverse_def
-- 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
inst_5 : CompleteSpace E
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) a
g : F → E
hg : ∀ᶠ (x : E) in 𝓝 a, g (f x) = x
⊢ HasStrictFDerivAt g (↑f'.symm : F →L[𝕜] E) (f a)

Tactic:
hf.to_localInverse.congr_of_eventuallyEq <| (hf.localInverse_unique hg).mono fun _ => Eq.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.Eventually.mono, HasStrictFDerivAt.to_localInverse, HasStrictFDerivAt.localInverse_unique, Eq.symm
-- 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
f : E → F
f' : E → E ≃L[𝕜] F
hf : ∀ (x : E), HasStrictFDerivAt f (↑(f' x) : E →L[𝕜] F) x
⊢ IsOpenMap f

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

Premises used: Iff.mpr, HasStrictFDerivAt.map_nhds_eq_of_equiv, Eq.ge, isOpenMap_iff_nhds_le
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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), LipschitzWith (lipschitzExtensionConstant F * c) u ∧ EqOn (f - (⇑f' : (a : E) → F)) u s

Tactic:
hf.lipschitzOnWith.extend_finite_dimension

Premises used: LipschitzOnWith.extend_finite_dimension, ApproximatesLinearOn.lipschitzOnWith
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)‖₊⁻¹
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
⊢ ∃ (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

Premises used: LipschitzOnWith.extend_finite_dimension, ApproximatesLinearOn.lipschitzOnWith
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)
simp_rw₂ : f x = HAdd.hAdd (α := F) ((f' : (a : E) → F) x : F) (HSub.hSub (β := F) (f x) ((f' : (a : E) → F) x : F))
⊢ f x = g x

Tactic:
simp_rw [g, ← uf hx, Pi.sub_apply, add_sub_cancel]

Premises used: add_sub_cancel, Pi.sub_apply
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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)
⊢ 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]
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
a : LipschitzOnWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F)) univ
⊢ ApproximatesLinearOn g (↑f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c)

Tactic:
apply LipschitzOnWith.approximatesLinearOn

Premises used: LipschitzOnWith.approximatesLinearOn
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
a : LipschitzWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F))
⊢ LipschitzOnWith (lipschitzExtensionConstant F * c) (g - (⇑(↑f' : E →L[ℝ] F) : (a : E) → F)) univ

Tactic:
rw [lipschitzOnWith_univ]

Premises used: lipschitzOnWith_univ
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional
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
⊢ LipschitzWith (lipschitzExtensionConstant F * c) u

Tactic:
hu