Theorem: mem_domain_self (Ray/Dynamics/Grow.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✝ : ℂ
a z : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
⊢ (c, x) ∈ {c} ×ˢ closedBall 0 (Complex.abs x)
Tactic:
simp only [mem_prod_eq, mem_singleton_iff, eq_self_iff_true, mem_closedBall, Complex.dist_eq,
  sub_zero, true_and_iff, le_refl]
State after:
no goals