case h0
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
hf : ContDiffAt 𝕜 0 (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 0 (↑(LocalHomeomorph.symm f)) a

case hsuc
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 (↑(Nat.succ n)) (↑(LocalHomeomorph.symm f)) a

case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 ⊤ (↑(LocalHomeomorph.symm f)) a
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 n (↑(LocalHomeomorph.symm f)) a
induction' n using ENat.nat_induction with n IH Itop
case h0
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
hf : ContDiffAt 𝕜 0 (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ∃ u, u ∈ 𝓝 a ∧ ContinuousOn (↑(LocalHomeomorph.symm f)) u
case h0
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
hf : ContDiffAt 𝕜 0 (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 0 (↑(LocalHomeomorph.symm f)) a
rw [contDiffAt_zero]
no goals
case h0
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
hf : ContDiffAt 𝕜 0 (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ∃ u, u ∈ 𝓝 a ∧ ContinuousOn (↑(LocalHomeomorph.symm f)) u
exact ⟨f.target, IsOpen.mem_nhds f.open_target ha, f.continuous_invFun⟩
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
⊢ ContDiffAt 𝕜 (↑(Nat.succ n)) (↑(LocalHomeomorph.symm f)) a
case hsuc
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 (↑(Nat.succ n)) (↑(LocalHomeomorph.symm f)) a
obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
⊢ ∃ f', (∃ u, u ∈ 𝓝 a ∧ ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' a
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
⊢ ContDiffAt 𝕜 (↑(Nat.succ n)) (↑(LocalHomeomorph.symm f)) a
apply contDiffAt_succ_iff_hasFDerivAt.mpr
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ∃ f', (∃ u, u ∈ 𝓝 a ∧ ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' a
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
⊢ ∃ f', (∃ u, u ∈ 𝓝 a ∧ ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' a
have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
case hsuc.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x

case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
case hsuc.intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ∃ f', (∃ u, u ∈ 𝓝 a ∧ ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' a
refine' ⟨inverse ∘ f' ∘ f.symm, _, _⟩
case hsuc.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
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₀'
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
obtain ⟨t, htu, ht, htf⟩ := mem_nhds_iff.mp (Filter.inter_mem hu h_nhds)
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t ∈ 𝓝 a ∧
    ∀ (x : F),
      x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t →
        HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ ∃ u,
    u ∈ 𝓝 a ∧
      ∀ (x : F), x ∈ u → HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
use f.target ∩ f.symm ⁻¹' t
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t)

case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ a ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t

case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ ∀ (x : F),
    x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t →
      HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t ∈ 𝓝 a ∧
    ∀ (x : F),
      x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t →
        HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
refine' ⟨IsOpen.mem_nhds _ _, _⟩
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ ∀ (x : F),
    x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t →
      HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
intro x hx
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
obtain ⟨hxu, e, he⟩ := htu hx.2
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
  rw [he]
  exact hff' (f.symm x) hxu
case h.e'_10
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑(LocalHomeomorph.symm f) x)
⊢ (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x = ↑(ContinuousLinearEquiv.symm e)
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_3.intro.intro
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑(LocalHomeomorph.symm f)) ((inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x) x
convert f.hasFDerivAt_symm hx.1 h_deriv
no goals
case h.e'_10
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑(LocalHomeomorph.symm f) x)
⊢ (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) x = ↑(ContinuousLinearEquiv.symm e)
simp [← he]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'✝ : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
hf₀' : range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 ↑f₀'
⊢ {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
have hf₀' := f₀'.nhds
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'✝ : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
hf₀' : range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' (↑(LocalHomeomorph.symm f) a))
⊢ {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'✝ : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
hf₀' : range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 ↑f₀'
⊢ {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
rw [← eq_f₀'] at hf₀'
no goals
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀'✝ : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
hf₀' : range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (f' (↑(LocalHomeomorph.symm f) a))
⊢ {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
exact hf'.continuousAt.preimage_mem_nhds hf₀'
no goals
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ IsOpen (f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t)
exact f.preimage_open_of_open_symm ht
no goals
case hsuc.intro.intro.intro.intro.refine'_1.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
⊢ a ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
exact mem_inter ha (mem_preimage.mpr htf)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑f) (f' (↑(LocalHomeomorph.symm f) x)) (↑(LocalHomeomorph.symm f) x)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑f) (↑e) (↑(LocalHomeomorph.symm f) x)
rw [he]
no goals
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t✝ u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen t
htf : ↑(LocalHomeomorph.symm f) a ∈ t
x : F
hx : x ∈ f.target ∩ ↑(LocalHomeomorph.symm f) ⁻¹' t
hxu : ↑(LocalHomeomorph.symm f) x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑(LocalHomeomorph.symm f) x)
⊢ HasFDerivAt (↑f) (f' (↑(LocalHomeomorph.symm f) x)) (↑(LocalHomeomorph.symm f) x)
exact hff' (f.symm x) hxu
case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
have h_deriv₁ : ContDiffAt 𝕜 n inverse (f' (f.symm a)) := by
  rw [eq_f₀']
  exact contDiffAt_map_inverse _
case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
h_deriv₂ : ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
have h_deriv₂ : ContDiffAt 𝕜 n f.symm a := by
  refine' IH (hf.of_le _)
  norm_cast
  exact Nat.le_succ n
no goals
case hsuc.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
h_deriv₂ : ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
⊢ ContDiffAt 𝕜 (↑n) (inverse ∘ f' ∘ ↑(LocalHomeomorph.symm f)) a
exact (h_deriv₁.comp _ hf').comp _ h_deriv₂
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) inverse ↑f₀'
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
rw [eq_f₀']
no goals
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) inverse ↑f₀'
exact contDiffAt_map_inverse _
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ ↑n ≤ ↑(Nat.succ n)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
refine' IH (hf.of_le _)
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ n ≤ Nat.succ n
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ ↑n ≤ ↑(Nat.succ n)
norm_cast
no goals
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
IH : ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 (↑(Nat.succ n)) (↑f) (↑(LocalHomeomorph.symm f) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑(LocalHomeomorph.symm f) a)
u : Set E
hu : u ∈ 𝓝 (↑(LocalHomeomorph.symm f) a)
hff' : ∀ (x : E), x ∈ u → HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑(LocalHomeomorph.symm f) a) = ↑f₀'
h_deriv₁ : ContDiffAt 𝕜 (↑n) inverse (f' (↑(LocalHomeomorph.symm f) a))
⊢ n ≤ Nat.succ n
exact Nat.le_succ n
case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ContDiffAt 𝕜 ⊤ (↑(LocalHomeomorph.symm f)) a
refine' contDiffAt_top.mpr _
case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
⊢ ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
⊢ ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
intro n
no goals
case htop
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁰ : NormedAddCommGroup D
inst✝⁹ : NormedSpace 𝕜 D
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type uG
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
X : Type ?u.2744530
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
inst✝ : CompleteSpace E
f : LocalHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(LocalHomeomorph.symm f) a)
hf✝ : ContDiffAt 𝕜 n✝ (↑f) (↑(LocalHomeomorph.symm f) a)
Itop : ∀ (n : ℕ), ContDiffAt 𝕜 (↑n) (↑f) (↑(LocalHomeomorph.symm f) a) → ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
hf : ContDiffAt 𝕜 ⊤ (↑f) (↑(LocalHomeomorph.symm f) a)
n : ℕ
⊢ ContDiffAt 𝕜 (↑n) (↑(LocalHomeomorph.symm f)) a
exact Itop n (contDiffAt_top.mp hf n)