awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 ω (↑f : E → F) ((↑f.symm : F → E) a)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) a

Tactic:
f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv

Premises used: OpenPartialHomeomorph.analyticAt_symm, HasFDerivAt.fderiv, ContDiffAt.analyticAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 ω (↑f : E → F) ((↑f.symm : F → E) a)
⊢ AnalyticAt 𝕜 (↑f.symm : F → E) a

Tactic:
exact f.analyticAt_symm ha hf.analyticAt hf₀'.fderiv

Premises used: OpenPartialHomeomorph.analyticAt_symm, HasFDerivAt.fderiv, ContDiffAt.analyticAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
zero : ∃ u ∈ 𝓝 a, ContinuousOn (↑f.symm : F → E) u
⊢ ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
apply contDiffAt_zero.2

Premises used: Iff.mpr, contDiffAt_zero
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ∃ u ∈ 𝓝 a, ContinuousOn (↑f.symm : F → E) u

Tactic:
⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩

Premises used: PartialEquiv.target, OpenPartialHomeomorph.continuousOn_invFun, And.intro, IsOpen.mem_nhds, Exists.intro, OpenPartialHomeomorph.open_target, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ∃ u ∈ 𝓝 a, ContinuousOn (↑f.symm : F → E) u

Tactic:
exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuousOn_invFun⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
succ :
  ∀ (f' : E → E →L[𝕜] F) (hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)) (u : Set E)
    (hu : u ∈ 𝓝 ((↑f.symm : F → E) a)) (hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x),
    ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
⊢ ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf

Premises used: contDiffAt_succ_iff_hasFDerivAt, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
succ :
  ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a
⊢ ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
apply contDiffAt_succ_iff_hasFDerivAt.2

Premises used: Iff.mpr, contDiffAt_succ_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
⊢ f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)

Tactic:
have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
⊢ ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a

Tactic:
⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩

Premises used: Function.comp, OpenPartialHomeomorph.toFun', And.intro, Exists.intro, ContinuousLinearMap.inverse, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
succ : ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
succ₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) (inverse ∘ f' ∘ (↑f.symm : F → E)) a
⊢ ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a

Tactic:
refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
⊢ range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑f₀' : E →L[𝕜] F)

Tactic:
have hf₀' := f₀'.nhds
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'_1 : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
hf₀' : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑f₀' : E →L[𝕜] F)
⊢ range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' ((↑f.symm : F → E) a))

Tactic:
rw [← eq_f₀'] at hf₀'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'_1 : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
hf₀' : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' ((↑f.symm : F → E) a))
⊢ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)

Tactic:
hf'.continuousAt.preimage_mem_nhds hf₀'

Premises used: Set.Mem, setOf, ContinuousAt.preimage_mem_nhds, Set.preimage, Set.range, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'_1 : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
hf₀' : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' ((↑f.symm : F → E) a))
⊢ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)

Tactic:
exact hf'.continuousAt.preimage_mem_nhds hf₀'

Premises used: ContinuousAt.preimage_mem_nhds, ContDiffAt.continuousAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
⊢ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)

Tactic:
have h_nhds : { y : E | ∃ e : E ≃L[𝕜] F, ↑e = f' y } ∈ 𝓝 (f.symm a) := by
          have hf₀' := f₀'.nhds
          rw [← eq_f₀'] at hf₀'
          exact hf'.continuousAt.preimage_mem_nhds hf₀'
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
succ :
  ∀ (t : Set E) (htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y})
    (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t) (htf : (↑f.symm : F → E) a ∈ t),
    ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)

Premises used: mem_nhds_iff, Filter.inter_mem, Iff.mp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
h :
  f.target ∩ (↑f.symm : F → E) ⁻¹' t ∈ 𝓝 a ∧
    ∀ x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
use f.target ∩ f.symm ⁻¹' t

Premises used: PartialEquiv.target, OpenPartialHomeomorph.toPartialEquiv, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
⊢ f.target ∩ (↑f.symm : F → E) ⁻¹' t ∈ 𝓝 a ∧
    ∀ x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
⟨IsOpen.mem_nhds ?_ ?_, ?_⟩

Premises used: And.intro, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
h : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.target ∩ (↑f.symm : F → E) ⁻¹' t)
h₁ : a ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
h₂ : ∀ x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
⊢ f.target ∩ (↑f.symm : F → E) ⁻¹' t ∈ 𝓝 a ∧
    ∀ x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.target ∩ (↑f.symm : F → E) ⁻¹' t)

Tactic:
f.isOpen_inter_preimage_symm ht

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.target ∩ (↑f.symm : F → E) ⁻¹' t)

Tactic:
exact f.isOpen_inter_preimage_symm ht

Premises used: OpenPartialHomeomorph.isOpen_inter_preimage_symm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
h_nhds : {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
t : Set E
htu : t ⊆ u ∩ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : (↑f.symm : F → E) a ∈ t
⊢ a ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t

Tactic:
mem_inter ha (mem_preimage.mpr htf)

Premises used: Iff.mpr, Set.mem_inter, Set.mem_preimage