Theorem: not_local_inj_of_mfderiv_zero (Ray/Dynamics/Multiple.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
generalize hg : (fun z ↦ extChartAt I (f c) (f ((extChartAt I c).symm z))) = g
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have dg : mfderiv I I g (extChartAt I c c) = 0 := by
  have fd : MDifferentiableAt I I f ((extChartAt I c).symm (extChartAt I c c)) := by
    rw [PartialEquiv.left_inv]; exact fa.mdifferentiableAt; apply mem_extChartAt_source
  rw [← hg, ←Function.comp_def, mfderiv_comp _ (HolomorphicAt.extChartAt _).mdifferentiableAt _,
    ←Function.comp_def, mfderiv_comp _ fd (HolomorphicAt.extChartAt_symm _).mdifferentiableAt,
    PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero]
  apply mem_extChartAt_source; apply mem_extChartAt_target; rw [PartialEquiv.left_inv]
  apply mem_extChartAt_source; apply mem_extChartAt_source
  exact MDifferentiableAt.comp _ fd
    (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
simp only [holomorphicAt_iff, Function.comp, hg] at fa
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
have dg' := fa.2.differentiableAt.mdifferentiableAt.hasMFDerivAt
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasMFDerivAt I I g (↑(extChartAt I c) c) (mfderiv I I g (↑(extChartAt I c) c))
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasMFDerivAt I I g (↑(extChartAt I c) c) (mfderiv I I g (↑(extChartAt I c) c))
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
rw [dg, hasMFDerivAt_iff_hasFDerivAt] at dg'
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
dg : mfderiv I I g (↑(extChartAt I c) c) = 0
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
replace dg := dg'.hasDerivAt
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg' : HasFDerivAt g 0 (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
clear dg'
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
rcases not_local_inj_of_deriv_zero fa.2 dg with ⟨h, ha, h0, e⟩
State after:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z

State before:
case intro.intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∃ g, HolomorphicAt I I g c ∧ g c = c ∧ ∀ᶠ (z : S) in 𝓝[≠] c, g z ≠ z ∧ f (g z) = f z
Tactic:
refine ⟨fun z ↦ (extChartAt I c).symm (h (extChartAt I c z)), ?_, ?_, ?_⟩
State after:
case intro.intro.intro.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c

case intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c = c

case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∀ᶠ (z : S) in 𝓝[≠] c,
    (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z ≠ z ∧
      f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0
Tactic:
have fd : MDifferentiableAt I I f ((extChartAt I c).symm (extChartAt I c c)) := by
  rw [PartialEquiv.left_inv]; exact fa.mdifferentiableAt; apply mem_extChartAt_source
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ mfderiv I I g (↑(extChartAt I c) c) = 0
Tactic:
rw [← hg, ←Function.comp_def, mfderiv_comp _ (HolomorphicAt.extChartAt _).mdifferentiableAt _,
  ←Function.comp_def, mfderiv_comp _ fd (HolomorphicAt.extChartAt_symm _).mdifferentiableAt,
  PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero]
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_source
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_target
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f (↑(extChartAt I c).symm (↑(extChartAt I c) c)) ∈ (extChartAt I (f c)).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
rw [PartialEquiv.left_inv]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f c ∈ (extChartAt I (f c)).source

case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ f c ∈ (extChartAt I (f c)).source

case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_source
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ c ∈ (extChartAt I c).source

S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
apply mem_extChartAt_source
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fd : MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
⊢ MDifferentiableAt I I (fun z => f (↑(extChartAt I c).symm z)) (↑(extChartAt I c) c)
Tactic:
exact MDifferentiableAt.comp _ fd
  (HolomorphicAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ MDifferentiableAt I I f (↑(extChartAt I c).symm (↑(extChartAt I c) c))
Tactic:
rw [PartialEquiv.left_inv]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ MDifferentiableAt I I f c

case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ c ∈ (extChartAt I c).source

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ MDifferentiableAt I I f c

case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ c ∈ (extChartAt I c).source
Tactic:
exact fa.mdifferentiableAt
State after:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ c ∈ (extChartAt I c).source

State before:
case h
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
fa : HolomorphicAt I I f c
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
⊢ c ∈ (extChartAt I c).source
Tactic:
apply mem_extChartAt_source
State after:
no goals

State before:
case intro.intro.intro.refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c
Tactic:
apply (HolomorphicAt.extChartAt_symm (mem_extChartAt_target I c)).comp_of_eq
State after:
case intro.intro.intro.refine_1.gh
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun x => h (↑(extChartAt I c) x)) c

case intro.intro.intro.refine_1.e
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

State before:
case intro.intro.intro.refine_1.gh
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ HolomorphicAt I I (fun x => h (↑(extChartAt I c) x)) c

case intro.intro.intro.refine_1.e
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
Tactic:
apply (ha.holomorphicAt I I).comp_of_eq
  (HolomorphicAt.extChartAt (mem_extChartAt_source I c)) rfl
State after:
case intro.intro.intro.refine_1.e
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

State before:
case intro.intro.intro.refine_1.e
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
Tactic:
exact h0
State after:
no goals

State before:
case intro.intro.intro.refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c = c
Tactic:
simp only [h0, PartialEquiv.left_inv _ (mem_extChartAt_source I c)]
State after:
no goals

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (z : ℂ) in 𝓝[≠] ↑(extChartAt I c) c, h z ≠ z ∧ g (h z) = g z
⊢ ∀ᶠ (z : S) in 𝓝[≠] c,
    (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z ≠ z ∧
      f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) z) = f z
Tactic:
rw [eventually_nhdsWithin_iff] at e ⊢
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ {c}ᶜ →
      (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
        f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ {c}ᶜ →
      (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
        f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
apply ((continuousAt_extChartAt I c).eventually e).mp
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
        h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
      x ∈ {c}ᶜ →
        (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
          f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
        h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
      x ∈ {c}ᶜ →
        (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
          f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
apply ((isOpen_extChartAt_source I c).eventually_mem (mem_extChartAt_source I c)).mp
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
have m2 : ∀ᶠ z in 𝓝 c, f z ∈ (extChartAt I (f c)).source :=
  fa.1.eventually_mem (extChartAt_source_mem_nhds I _)
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3 : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
⊢ ∀ᶠ (x : S) in 𝓝 c,
    x ∈ (extChartAt I c).source →
      (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
          h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
        x ∈ {c}ᶜ →
          (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
            f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
refine m1.mp (m2.mp (m3.mp (eventually_of_forall ?_)))
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3 : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ∈ {c}ᶜ →
                (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
                  f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3 : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ∈ {↑(extChartAt I c) c}ᶜ →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ∈ {c}ᶜ →
                (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x ≠ x ∧
                  f ((fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) x) = f x
Tactic:
simp only [mem_compl_singleton_iff]
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3 : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ≠ ↑(extChartAt I c) c →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ≠ c →
                ↑(extChartAt I c).symm (h (↑(extChartAt I c) x)) ≠ x ∧
                  f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) = f x

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3 : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
⊢ ∀ (x : S),
    f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) ∈ (extChartAt I (f c)).source →
      f x ∈ (extChartAt I (f c)).source →
        h (↑(extChartAt I c) x) ∈ (extChartAt I c).target →
          x ∈ (extChartAt I c).source →
            (↑(extChartAt I c) x ≠ ↑(extChartAt I c) c →
                h (↑(extChartAt I c) x) ≠ ↑(extChartAt I c) x ∧ g (h (↑(extChartAt I c) x)) = g (↑(extChartAt I c) x)) →
              x ≠ c →
                ↑(extChartAt I c).symm (h (↑(extChartAt I c) x)) ≠ x ∧
                  f (↑(extChartAt I c).symm (h (↑(extChartAt I c) x))) = f x
Tactic:
intro z m3 m2 m1 m0 even zc
State after:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
case intro.intro.intro.refine_3
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rcases even ((PartialEquiv.injOn _).ne m0 (mem_extChartAt_source I c) zc) with ⟨hz, gh⟩
State after:
case intro.intro.intro.refine_3.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
case intro.intro.intro.refine_3.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z ∧ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
constructor
State after:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z

case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
Tactic:
refine ContinuousAt.eventually_mem ?_ (extChartAt_target_mem_nhds' I ?_)
State after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ContinuousAt (fun z => h (↑(extChartAt I c) z)) c

case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ h (↑(extChartAt I c) c) ∈ (extChartAt I c).target

State before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ContinuousAt (fun z => h (↑(extChartAt I c) z)) c
Tactic:
exact ha.continuousAt.comp_of_eq (continuousAt_extChartAt I c) rfl
State after:
no goals

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ h (↑(extChartAt I c) c) ∈ (extChartAt I c).target
Tactic:
rw [h0]
State after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
⊢ ↑(extChartAt I c) c ∈ (extChartAt I c).target
Tactic:
exact mem_extChartAt_target I c
State after:
no goals

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
Tactic:
refine ContinuousAt.eventually_mem ?_ (extChartAt_source_mem_nhds' I ?_)
State after:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) c

case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) c))) ∈ (extChartAt I (f c)).source

State before:
case refine_1
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) c
Tactic:
apply fa.1.comp_of_eq
State after:
case refine_1.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => ↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
apply (continuousAt_extChartAt_symm I _).comp_of_eq
State after:
case refine_1.hf.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => h (↑(extChartAt I c) z)) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hf.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => h (↑(extChartAt I c) z)) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
apply ha.continuousAt.comp_of_eq
State after:
case refine_1.hf.hf.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => ↑(extChartAt I c) z) c

case refine_1.hf.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hf.hf.hf
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ContinuousAt (fun z => ↑(extChartAt I c) z) c

case refine_1.hf.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
exact continuousAt_extChartAt I _
State after:
case refine_1.hf.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hf.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c) c = ↑(extChartAt I c) c

case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
rfl
State after:
case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hf.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ h (↑(extChartAt I c) c) = ↑(extChartAt I c) c

case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
exact h0
State after:
case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c

State before:
case refine_1.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) c)) = c
Tactic:
rw [h0, PartialEquiv.left_inv _ (mem_extChartAt_source I _)]
State after:
no goals

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) c))) ∈ (extChartAt I (f c)).source
Tactic:
rw [h0, PartialEquiv.left_inv _ (mem_extChartAt_source I _)]
State after:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ f c ∈ (extChartAt I (f c)).source

State before:
case refine_2
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1 : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2 : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
⊢ f c ∈ (extChartAt I (f c)).source
Tactic:
apply mem_extChartAt_source
State after:
no goals

State before:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ z
Tactic:
nth_rw 2 [← PartialEquiv.left_inv _ m0]
State after:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ ↑(extChartAt I c).symm (↑(extChartAt I c) z)

State before:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c).symm (h (↑(extChartAt I c) z)) ≠ ↑(extChartAt I c).symm (↑(extChartAt I c) z)
Tactic:
rw [(PartialEquiv.injOn _).ne_iff]
State after:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z

case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).symm.source

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source

State before:
case intro.intro.intro.refine_3.intro.left
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z

case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).symm.source

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source
Tactic:
exact hz
State after:
case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).symm.source

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source

State before:
case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).symm.source

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source
Tactic:
rw [PartialEquiv.symm_source]
State after:
case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).target

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source

State before:
case intro.intro.intro.refine_3.intro.left.hx
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ h (↑(extChartAt I c) z) ∈ (extChartAt I c).target

case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source
Tactic:
exact m1
State after:
case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source

State before:
case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).symm.source
Tactic:
rw [PartialEquiv.symm_source]
State after:
case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).target

State before:
case intro.intro.intro.refine_3.intro.left.hy
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ ↑(extChartAt I c) z ∈ (extChartAt I c).target
Tactic:
exact PartialEquiv.map_source _ m0
State after:
no goals

State before:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
simp only [← hg] at gh
State after:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh :
  ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) =
    ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (↑(extChartAt I c) z)))
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh :
  ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) =
    ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (↑(extChartAt I c) z)))
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rw [PartialEquiv.left_inv _ m0] at gh
State after:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) = ↑(extChartAt I (f c)) (f z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z)))) = ↑(extChartAt I (f c)) (f z)
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
rw [(PartialEquiv.injOn _).eq_iff m3 m2] at gh
State after:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z

State before:
case intro.intro.intro.refine_3.intro.right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
inst✝³ : AnalyticManifold I S
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f : S → T
c : S
df : mfderiv I I f c = 0
g : ℂ → ℂ
hg : (fun z => ↑(extChartAt I (f c)) (f (↑(extChartAt I c).symm z))) = g
fa : ContinuousAt f c ∧ AnalyticAt ℂ g (↑(extChartAt I c) c)
dg : HasDerivAt g (0 1) (↑(extChartAt I c) c)
h : ℂ → ℂ
ha : AnalyticAt ℂ h (↑(extChartAt I c) c)
h0 : h (↑(extChartAt I c) c) = ↑(extChartAt I c) c
e : ∀ᶠ (x : ℂ) in 𝓝 (↑(extChartAt I c) c), x ∈ {↑(extChartAt I c) c}ᶜ → h x ≠ x ∧ g (h x) = g x
m1✝ : ∀ᶠ (z : S) in 𝓝 c, h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m2✝ : ∀ᶠ (z : S) in 𝓝 c, f z ∈ (extChartAt I (f c)).source
m3✝ : ∀ᶠ (z : S) in 𝓝 c, f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
z : S
m3 : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) ∈ (extChartAt I (f c)).source
m2 : f z ∈ (extChartAt I (f c)).source
m1 : h (↑(extChartAt I c) z) ∈ (extChartAt I c).target
m0 : z ∈ (extChartAt I c).source
even :
  ↑(extChartAt I c) z ≠ ↑(extChartAt I c) c →
    h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z ∧ g (h (↑(extChartAt I c) z)) = g (↑(extChartAt I c) z)
zc : z ≠ c
hz : h (↑(extChartAt I c) z) ≠ ↑(extChartAt I c) z
gh : f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
⊢ f (↑(extChartAt I c).symm (h (↑(extChartAt I c) z))) = f z
Tactic:
exact gh
State after:
no goals