Theorem: Super.post_slice_connected (Ray/Dynamics/Bottcher.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ IsConnected {z | (c, z) ∈ s.post}
Tactic:
have e : {z | (c, z) ∈ s.post} = s.homeomorphSlice c '' {x | (c, x) ∈ s.ext} :=
  (s.homeomorphSlice c).image_source_eq_target.symm
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected {z | (c, z) ∈ s.post}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected {z | (c, z) ∈ s.post}
Tactic:
rw [e]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected (↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext})

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
e : {z | (c, z) ∈ s.post} = ↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext}
⊢ IsConnected (↑(s.homeomorphSlice c) '' {x | (c, x) ∈ s.ext})
Tactic:
exact (s.ext_slice_connected c).image _ (s.homeomorphSlice c).continuousOn
State after:
no goals