Theorem: Super.ext_connected (Ray/Dynamics/Ray.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
⊢ IsConnected s.ext
Tactic:
refine ⟨⟨(0, 0), s.mem_ext 0⟩, isPreconnected_of_forall (0, 0) ?_⟩
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
⊢ ∀ y ∈ s.ext, ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ y ∈ t ∧ IsPreconnected t

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
⊢ ∀ y ∈ s.ext, ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
intro ⟨c, x⟩ m
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ (c, x) ∈ t ∧ IsPreconnected t

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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ t ⊆ s.ext, (0, 0) ∈ t ∧ (c, x) ∈ t ∧ IsPreconnected t
Tactic:
use(fun x ↦ (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0}
State after:
case h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ⊆ s.ext ∧
    (0, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
      (c, x) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
        IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})

State before:
case h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ⊆ s.ext ∧
    (0, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
      (c, x) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0} ∧
        IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
simp only [mem_image, mem_union, union_subset_iff, mem_setOf, mem_prod_eq, mem_univ,
  true_and_iff, mem_singleton_iff, eq_self_iff_true, or_true_iff]
State after:
case h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext ∧ univ ×ˢ {0} ⊆ s.ext) ∧
    ((∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0) ∧
      IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})

State before:
case h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext ∧ univ ×ˢ {0} ⊆ s.ext) ∧
    ((∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0) ∧
      IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
State after:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext

case h.refine_2
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ univ ×ˢ {0} ⊆ s.ext

case h.refine_3
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0

case h.refine_4
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})

State before:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ⊆ s.ext
Tactic:
intro y n
State after:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : y ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
⊢ y ∈ s.ext

State before:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : y ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
⊢ y ∈ s.ext
Tactic:
simp only [mem_image, mem_setOf] at n
State after:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : ∃ x, (c, x) ∈ s.ext ∧ (c, x) = y
⊢ y ∈ s.ext

State before:
case h.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
y : ℂ × ℂ
n : ∃ x, (c, x) ∈ s.ext ∧ (c, x) = y
⊢ y ∈ s.ext
Tactic:
rcases n with ⟨x, m, e⟩
State after:
case h.refine_1.intro.intro
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 x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : (c, x) ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext

State before:
case h.refine_1.intro.intro
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 x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : (c, x) ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Tactic:
rw [e] at m
State after:
case h.refine_1.intro.intro
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 x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : y ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext

State before:
case h.refine_1.intro.intro
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 x✝ : ℂ
m✝ : (c, x✝) ∈ s.ext
y : ℂ × ℂ
x : ℂ
m : y ∈ s.ext
e : (c, x) = y
⊢ y ∈ s.ext
Tactic:
exact m
State after:
no goals

State before:
case h.refine_2
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ univ ×ˢ {0} ⊆ s.ext
Tactic:
intro ⟨c, x⟩ m
State after:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : (c, x) ∈ univ ×ˢ {0}
⊢ (c, x) ∈ s.ext

State before:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : (c, x) ∈ univ ×ˢ {0}
⊢ (c, x) ∈ s.ext
Tactic:
simp only [mem_prod_eq, mem_singleton_iff] at m
State after:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, x) ∈ s.ext

State before:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, x) ∈ s.ext
Tactic:
rw [m.2]
State after:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, 0) ∈ s.ext

State before:
case h.refine_2
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✝ x✝ : ℂ
m✝ : (c✝, x✝) ∈ s.ext
c x : ℂ
m : c ∈ univ ∧ x = 0
⊢ (c, 0) ∈ s.ext
Tactic:
exact s.mem_ext c
State after:
no goals

State before:
case h.refine_3
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)) ∨ x = 0
Tactic:
left
State after:
case h.refine_3.h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)

State before:
case h.refine_3.h
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ ∃ x_1, (c, x_1) ∈ s.ext ∧ (c, x_1) = (c, x)
Tactic:
exact ⟨x, m, rfl⟩
State after:
no goals

State before:
case h.refine_4
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext} ∪ univ ×ˢ {0})
Tactic:
refine IsPreconnected.union (c, 0) ?_ ?_ ?_ ?_
State after:
case h.refine_4.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}

case h.refine_4.refine_2
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ univ ×ˢ {0}

case h.refine_4.refine_3
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext})

case h.refine_4.refine_4
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected (univ ×ˢ {0})

State before:
case h.refine_4.refine_1
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ (fun x => (c, x)) '' {x | (c, x) ∈ s.ext}
Tactic:
use 0, s.mem_ext c
State after:
no goals

State before:
case h.refine_4.refine_2
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ (c, 0) ∈ univ ×ˢ {0}
Tactic:
exact mk_mem_prod (mem_univ _) rfl
State after:
no goals

State before:
case h.refine_4.refine_3
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected ((fun x => (c, x)) '' {x | (c, x) ∈ s.ext})
Tactic:
exact IsPreconnected.image (s.ext_slice_connected c).isPreconnected _
  (Continuous.Prod.mk _).continuousOn
State after:
no goals

State before:
case h.refine_4.refine_4
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 x : ℂ
m : (c, x) ∈ s.ext
⊢ IsPreconnected (univ ×ˢ {0})
Tactic:
exact isPreconnected_univ.prod isPreconnected_singleton
State after:
no goals