Theorem: Super.ext_slice (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
c : ℂ
⊢ {x | (c, x) ∈ s.ext} = ball 0 (s.p c)
Tactic:
apply Set.ext
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
c : ℂ
⊢ ∀ (x : ℂ), x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)

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
c : ℂ
⊢ ∀ (x : ℂ), x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Tactic:
intro x
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
c x : ℂ
⊢ x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)

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
c x : ℂ
⊢ x ∈ {x | (c, x) ∈ s.ext} ↔ x ∈ ball 0 (s.p c)
Tactic:
simp only [Super.ext, mem_ball, mem_setOf, Complex.dist_eq, sub_zero]
State after:
no goals