Theorem: Super.fl0 (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 : ℕ
s : Super f d a
c : ℂ
⊢ s.fl c 0 = 0
Tactic:
simp only [Super.fl, _root_.fl, s.f0, Function.comp_apply, zero_add, PartialEquiv.left_inv,
  mem_extChartAt_source, sub_self]
State after:
no goals