awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
this : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 (dfu.implicitFunctionOfProdDomain if₂u u.1))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)),
    Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
⊢ Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)

Tactic:
rwa [(dfu.eventually_apply_eq_iff_implicitFunctionOfProdDomain if₂u).self_of_nhds.mp rfl] at this

Premises used: Filter.Eventually.self_of_nhds, HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain, Iff.mp, rfl
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
⊢ Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)

Tactic:
have hψ := dfu.tendsto_implicitFunctionOfProdDomain if₂u
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
hψ : Tendsto (dfu.implicitFunctionOfProdDomain if₂u) (𝓝 u.1) (𝓝 u.2)
set :
  let ψ := dfu.implicitFunctionOfProdDomain if₂u;
  ∀ (hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)), ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, dfu.implicitFunctionOfProdDomain if₂u x) = f u

Tactic:
set ψ := dfu.implicitFunctionOfProdDomain if₂u

Premises used: HasStrictFDerivAt.implicitFunctionOfProdDomain
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
this : ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
suffices : ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u

Tactic:
suffices ∀ᶠ x in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x by simpa using this
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
apply : ∀ᶠ (p : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, f (p.1, p.2) = f u ↔ ψ p.1 = p.2
⊢ ∀ᶠ (x : E₁) in 𝓝 u.1, f (x, ψ x) = f u ↔ ψ x = ψ x

Tactic:
apply Eventually.image_of_prod (r := fun x y => f (x, y) = f u ↔ ψ x = y) hψ

Premises used: Filter.Eventually.image_of_prod
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
rw : ∀ᶠ (p : E₁ × E₂) in 𝓝 (u.1, u.2), f (p.1, p.2) = f u ↔ ψ p.1 = p.2
⊢ ∀ᶠ (p : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, f (p.1, p.2) = f u ↔ ψ p.1 = p.2

Tactic:
rw [← nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (p : E₁ × E₂) in 𝓝 (u.1, u.2), f (p.1, p.2) = f u ↔ ψ p.1 = p.2

Tactic:
dfu.eventually_apply_eq_iff_implicitFunctionOfProdDomain if₂u

Premises used: HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain
-- Module: Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E₁ : Type u_2
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : CompleteSpace E₁
E₂ : Type u_3
inst_4 : NormedAddCommGroup E₂
inst_5 : NormedSpace 𝕜 E₂
inst_6 : CompleteSpace E₂
F : Type u_4
inst_7 : NormedAddCommGroup F
inst_8 : NormedSpace 𝕜 F
inst_9 : CompleteSpace F
u : E₁ × E₂
f : E₁ × E₂ → F
f'u : E₁ × E₂ →L[𝕜] F
dfu : HasStrictFDerivAt (𝕜 := 𝕜) f f'u u
if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible
ψ : E₁ → E₂ := dfu.implicitFunctionOfProdDomain if₂u
hψ : Tendsto ψ (𝓝 u.1) (𝓝 u.2)
⊢ ∀ᶠ (p : E₁ × E₂) in 𝓝 (u.1, u.2), f (p.1, p.2) = f u ↔ ψ p.1 = p.2

Tactic:
exact dfu.eventually_apply_eq_iff_implicitFunctionOfProdDomain if₂u

Premises used: HasStrictFDerivAt.eventually_apply_eq_iff_implicitFunctionOfProdDomain
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
⊢ HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x

Tactic:
have hfd : HasStrictFDerivAt f i.toContinuousLinearMap x := hf.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
⊢ x ∈ R.source

Tactic:
have hx : x ∈ R.source := HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source _
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

Tactic:
R.hasFPowerSeriesAt_symm hx hf.hasFPowerSeriesAt (i := i) ?_ |>.analyticAt

Premises used: HasStrictFDerivAt.localInverse, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.hasFPowerSeriesAt_symm, AnalyticAt.hasFPowerSeriesAt, HasFPowerSeriesAt.analyticAt
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
refine :
  Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
    (FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
        (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
      (↑i : 𝕜 →L[𝕜] 𝕜))
⊢ AnalyticAt 𝕜 (HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf') (f x)

Tactic:
refine R.hasFPowerSeriesAt_symm hx hf.hasFPowerSeriesAt (i := i) ?_ |>.analyticAt

Premises used: OpenPartialHomeomorph.hasFPowerSeriesAt_symm, AnalyticAt.hasFPowerSeriesAt, HasFPowerSeriesAt.analyticAt
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
h :
  Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1 :
          (a : (i : Fin 1) → 𝕜) → 𝕜)
        fun (x : Fin 1) ↦ 1 :
      𝕜)
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
                (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
              (↑i : 𝕜 →L[𝕜] 𝕜) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜) :
          (a : (i : Fin 1) → 𝕜) → 𝕜)
        fun (x : Fin 1) ↦ 1 :
      𝕜)
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
    (FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
        (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
      (↑i : 𝕜 →L[𝕜] 𝕜))

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
i : 𝕜 ≃L[𝕜] 𝕜 := (ContinuousLinearEquiv.unitsEquivAut 𝕜 : (a : 𝕜ˣ) → 𝕜 ≃L[𝕜] 𝕜) (Units.mk0 (deriv f x) hf')
hfd : HasStrictFDerivAt (𝕜 := 𝕜) f (↑i : 𝕜 →L[𝕜] 𝕜) x
R : OpenPartialHomeomorph 𝕜 𝕜 := HasStrictFDerivAt.toOpenPartialHomeomorph f hfd
hx : x ∈ R.source
⊢ Eq (α := 𝕜)
    ((FormalMultilinearSeries.ofScalars 𝕜 (fun (n : ℕ) ↦ iteratedDeriv n f x / (↑n.factorial : 𝕜)) 1 :
          (a : (i : Fin 1) → 𝕜) → 𝕜)
        fun (x : Fin 1) ↦ 1 :
      𝕜)
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 𝕜 𝕜) :
                (a : 𝕜 →L[𝕜] 𝕜) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜)
              (↑i : 𝕜 →L[𝕜] 𝕜) :
            ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ 𝕜) 𝕜) :
          (a : (i : Fin 1) → 𝕜) → 𝕜)
        fun (x : Fin 1) ↦ 1 :
      𝕜)

Tactic:
simp [i]
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
⊢ AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)

Tactic:
⟨fun hg ↦ ?_, (AnalyticAt.comp · hf)⟩

Premises used: Iff.intro, AnalyticAt.comp
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
refine : ∀ (hg : AnalyticAt 𝕜 (g ∘ f) x), AnalyticAt 𝕜 g (f x)
⊢ AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x)

Tactic:
refine ⟨fun hg ↦ ?_, (AnalyticAt.comp · hf)⟩
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
⊢ AnalyticAt 𝕜 r (f x)

Tactic:
have hra : AnalyticAt 𝕜 r (f x) := hf.analyticAt_localInverse hf'
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
⊢ r (f x) = x

Tactic:
have : r (f x) = x := HasStrictFDerivAt.localInverse_apply_image ..
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 (g ∘ f) (r (f x))

Tactic:
rw [← this] at hg
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
hg₁ : AnalyticAt 𝕜 (g ∘ f) (r (f x))
⊢ AnalyticAt 𝕜 r (f x)

Tactic:
rw [← this] at hg
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
hg : AnalyticAt 𝕜 (g ∘ f) x
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
hg₁ : AnalyticAt 𝕜 (g ∘ f) (r (f x))
hra₁ : AnalyticAt 𝕜 r (f x)
⊢ r (f x) = x

Tactic:
rw [← this] at hg
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hg : AnalyticAt 𝕜 (g ∘ f) (r (f x))
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
(hg.comp hra).congr <| .fun_comp (HasStrictDerivAt.eventually_right_inverse ..) g

Premises used: HasStrictDerivAt.eventually_right_inverse, AnalyticAt.congr, Filter.EventuallyEq.fun_comp, AnalyticAt.comp
-- Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : CharZero 𝕜
E : Type u_2
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
g : 𝕜 → E
hf : AnalyticAt 𝕜 f x
hf' : deriv f x ≠ 0
r : 𝕜 → 𝕜 := HasStrictDerivAt.localInverse f (deriv f x) x ⋯ hf'
hg : AnalyticAt 𝕜 (g ∘ f) (r (f x))
hra : AnalyticAt 𝕜 r (f x)
this : r (f x) = x
⊢ AnalyticAt 𝕜 g (f x)

Tactic:
exact (hg.comp hra).congr <| .fun_comp (HasStrictDerivAt.eventually_right_inverse ..) g

Premises used: AnalyticAt.congr, AnalyticAt.comp
-- 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
⊢ ApproximatesLinearOn f f' ∅ c

Tactic:
simp [ApproximatesLinearOn]

Premises used: ApproximatesLinearOn
-- 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 c' : ℝ≥0
hc : c ≤ c'
hf : ApproximatesLinearOn f f' s c
x : E
hx : x ∈ s
y : E
hy : y ∈ s
ha : 0 ≤ ‖x - y‖
⊢ (↑c : ℝ) * ‖x - y‖ ≤ (↑c' : ℝ) * ‖x - y‖

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 t : Set E
c : ℝ≥0
hst : s ⊆ t
hf : ApproximatesLinearOn f f' t c
⊢ ApproximatesLinearOn f f' s c

Tactic:
fun x hx y hy ↦ hf x (hst hx) y (hst hy)

Premises used: ApproximatesLinearOn
-- 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
x y : E
simp :
  f x - f y - HSub.hSub (α := F) (β := F) ((f' : (a : E) → F) x : F) ((f' : (a : E) → F) y : F) =
    HSub.hSub (β := F) (f x) ((f' : (a : E) → F) x : F) - HSub.hSub (β := F) (f y) ((f' : (a : E) → F) y : F)
⊢ HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F) =
    HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x - HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) y

Tactic:
simp only [map_sub, Pi.sub_apply]

Premises used: map_sub, Pi.sub_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
x y : E
⊢ f x - f y - HSub.hSub (α := F) (β := F) ((f' : (a : E) → F) x : F) ((f' : (a : E) → F) y : F) =
    HSub.hSub (β := F) (f x) ((f' : (a : E) → F) x : F) - HSub.hSub (β := F) (f y) ((f' : (a : E) → F) y : 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
⊢ ∀ (x y : E),
    HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F) =
      HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x - HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) y

Tactic:
have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y := fun x y ↦ by
    simp only [map_sub, Pi.sub_apply]; 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
this :
  ∀ (x y : E),
    HSub.hSub (β := F) (f x - f y) ((f' : (a : E) → F) (x - y) : F) =
      HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) x - HSub.hSub (β := (a : E) → F) f (⇑f' : (a : E) → F) y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - (⇑f' : (a : E) → F)) s

Tactic:
simp only [this, lipschitzOnWith_iff_norm_sub_le, ApproximatesLinearOn]

Premises used: ApproximatesLinearOn, lipschitzOnWith_iff_norm_sub_le
-- 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' s c
⊢ LipschitzWith.{u_2, u_3} (β := F) c fun (x : (↑s : Type u_2)) ↦
    HSub.hSub (β := F) (f (↑x : E)) ((f' : (a : E) → F) (↑x : E) : F)

Tactic:
hf.lipschitzOnWith.to_restrict

Premises used: LipschitzOnWith.to_restrict, Set.restrict, ApproximatesLinearOn.lipschitzOnWith
-- 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' s c
⊢ LipschitzWith (‖f'‖₊ + c) (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
simpa only [restrict_apply, add_sub_cancel] using
    (f'.lipschitz.restrict s).add hf.lipschitz_sub

Premises used: Set.restrict_apply, ContinuousLinearMap.lipschitz, ApproximatesLinearOn.lipschitz_sub, LipschitzWith.add, LipschitzWith.restrict, add_sub_cancel
-- 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' s c
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (s.restrict (π := fun (a : E) ↦ F) f)

Tactic:
hf.lipschitz.continuous

Premises used: ApproximatesLinearOn.lipschitz, LipschitzWith.continuous