Theorem: prod_zero_mem_ball (Ray/Dynamics/BottcherNearM.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 : ℕ
c b : ℂ
r : ℝ
m : b ∈ ball c r
⊢ (b, 0) ∈ ball (c, 0) r
Tactic:
simp only [Metric.mem_ball] at 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✝ : ℂ
a z : S
d n : ℕ
c b : ℂ
r : ℝ
m : dist b c < r
⊢ (b, 0) ∈ ball (c, 0) r

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 : ℕ
c b : ℂ
r : ℝ
m : dist b c < r
⊢ (b, 0) ∈ ball (c, 0) r
Tactic:
simpa only [Metric.mem_ball, dist_prod_same_right]
State after:
no goals