awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
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)
⊢ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
have hf₀'₁ : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' ((↑f.symm : F → E) a))
Tactic: rw [← eq_f₀'] at hf₀'
Cleared hypotheses: hf₀'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
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)
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have h_nhds : {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₀'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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)
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have 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
Tactic: obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have 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
Tactic: use f.target ∩ f.symm ⁻¹' t
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
have h : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f.target ∩ (↑f.symm : F → E) ⁻¹' t)
Tactic: refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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)
⊢ 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
have h₁ : a ∈ f.target ∩ (↑f.symm : F → E) ⁻¹' t
Tactic: refine ⟨IsOpen.mem_nhds ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ 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
have h₂ : ∀ 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 ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
⊢ HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have 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
Tactic: obtain ⟨hxu, e, he⟩ := htu hx.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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)
have rw : HasFDerivAt (↑f : E → F) (f' ((↑f.symm : F → E) x)) ((↑f.symm : F → E) x)
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
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.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have h_deriv : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
have h : (inverse ∘ f' ∘ (↑f.symm : F → E)) x = (↑e.symm : F →L[𝕜] E)
Tactic: convert! f.hasFDerivAt_symm hx.1 h_deriv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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))
have rw : ContDiffAt 𝕜 (↑n : ℕ∞ω) inverse (↑f₀' : E →L[𝕜] F)
Tactic: rw [eq_f₀']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
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
have h_deriv₁ : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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
have refine : LE.le (α := ℕ∞ω) (↑(↑n : ℕ∞) : ℕ∞ω) (↑(↑n.succ : ℕ∞) : ℕ∞ω)
Tactic: refine IH (hf.of_le ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
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))
⊢ LE.le (α := ℕ∞ω) (↑(↑n : ℕ∞) : ℕ∞ω) (↑(↑n.succ : ℕ∞) : ℕ∞ω)
have norm_cast : n ≤ n.succ
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
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 : ℕ∞ω) (inverse ∘ f' ∘ (↑f.symm : F → E)) a
have h_deriv₂ : 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