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_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:
exact mem_inter ha (mem_preimage.mpr htf)

Premises used: Iff.mpr, Set.mem_inter, Set.mem_preimage
-- 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
h :
  ∀ (hxu : (↑f.symm : F → E) x ∈ u) (e : E ≃L[𝕜] F) (he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)),
    HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
⊢ HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
obtain ⟨hxu, e, he⟩ := htu hx.2

Premises used: And.right
-- 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
rw : HasFDerivAt (↑f : E → F) (f' ((↑f.symm : F → E) x)) ((↑f.symm : F → E) x)
⊢ HasFDerivAt (↑f : E → F) (↑e : E →L[𝕜] F) ((↑f.symm : F → E) x)

Tactic:
rw [he]
-- 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
⊢ HasFDerivAt (↑f : E → F) (f' ((↑f.symm : F → E) x)) ((↑f.symm : F → E) x)

Tactic:
hff' (f.symm x) hxu

Premises used: OpenPartialHomeomorph.toFun', 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
⊢ HasFDerivAt (↑f : E → F) (f' ((↑f.symm : F → E) x)) ((↑f.symm : F → E) x)

Tactic:
exact hff' (f.symm x) hxu

Premises used: OpenPartialHomeomorph.toFun', 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
⊢ HasFDerivAt (↑f : E → F) (↑e : E →L[𝕜] F) ((↑f.symm : F → E) x)

Tactic:
have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu
-- 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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
h_deriv : HasFDerivAt (↑f : E → F) (↑e : E →L[𝕜] F) ((↑f.symm : F → E) x)
⊢ HasFDerivAt (↑f.symm : F → E) (↑e.symm : F →L[𝕜] E) x

Tactic:
f.hasFDerivAt_symm hx.1 h_deriv

Premises used: And.left, OpenPartialHomeomorph.hasFDerivAt_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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
h_deriv : HasFDerivAt (↑f : E → F) (↑e : E →L[𝕜] F) ((↑f.symm : F → E) x)
h : (inverse ∘ f' ∘ (↑f.symm : F → E)) x = (↑e.symm : F →L[𝕜] E)
⊢ HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x

Tactic:
convert! f.hasFDerivAt_symm hx.1 h_deriv

Premises used: And.left, OpenPartialHomeomorph.hasFDerivAt_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
x : F
hx : x ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
hxu : (↑f.symm : F → E) x ∈ u
e : E ≃L[𝕜] F
he : (↑e : E →L[𝕜] F) = f' ((↑f.symm : F → E) x)
h_deriv : HasFDerivAt (↑f : E → F) (↑e : E →L[𝕜] F) ((↑f.symm : F → E) x)
⊢ (inverse ∘ f' ∘ (↑f.symm : F → E)) x = (↑e.symm : F →L[𝕜] E)

Tactic:
simp [← he]
-- 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)
rw : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (↑f₀' : E →L[𝕜] F)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))

Tactic:
rw [eq_f₀']
-- 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)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (↑f₀' : E →L[𝕜] F)

Tactic:
contDiffAt_map_inverse _

Premises used: contDiffAt_map_inverse
-- 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)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (↑f₀' : E →L[𝕜] F)

Tactic:
exact contDiffAt_map_inverse _

Premises used: contDiffAt_map_inverse
-- 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)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))

Tactic:
have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
          rw [eq_f₀']
          exact contDiffAt_map_inverse _
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
IH (hf.of_le ?_)

Premises used: ContDiffAt.of_le
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
refine : LE.le (α := ℕ∞ω) (↑(↑n : ℕ∞) : ℕ∞ω) (↑(↑n.succ : ℕ∞) : ℕ∞ω)
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
refine IH (hf.of_le ?_)

Premises used: ContDiffAt.of_le
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
norm_cast : n ≤ n.succ
⊢ LE.le (α := ℕ∞ω) (↑(↑n : ℕ∞) : ℕ∞ω) (↑(↑n.succ : ℕ∞) : ℕ∞ω)

Tactic:
norm_cast
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
⊢ n ≤ n.succ

Tactic:
Nat.le_succ n

Premises used: Nat.le_succ
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
⊢ n ≤ n.succ

Tactic:
exact Nat.le_succ n

Premises used: Nat.le_succ
-- 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_deriv₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (f' ((↑f.symm : F → E) a))
⊢ ContDiffAt 𝕜 (↑n : ℕ∞ω) (↑f.symm : F → E) a

Tactic:
have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
          refine IH (hf.of_le ?_)
          norm_cast
          exact Nat.le_succ n