Theorem: Eqn.congr (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
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
⊢ Eqn s n r1 x
Tactic:
have s := loc.self_of_nhds
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : uncurry r0 x = uncurry r1 x
⊢ Eqn s✝ n r1 x

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
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : uncurry r0 x = uncurry r1 x
⊢ Eqn s✝ n r1 x
Tactic:
simp only [uncurry] at s
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 : ℕ
p : ℝ
s✝ : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ Eqn s✝ n r1 x

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
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ Eqn s✝ n r1 x
Tactic:
exact
  { holo := e.holo.congr loc
    near := by simp only [← s, e.near]
    eqn := by simp only [← s, e.eqn] }
State after:
no goals

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
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ (x.1, (f x.1)^[n] (r1 x.1 x.2)) ∈ s✝.near
Tactic:
simp only [← s, e.near]
State after:
no goals

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
x : ℂ × ℂ
r0 r1 : ℂ → ℂ → S
e : Eqn s✝ n r0 x
loc : (𝓝 x).EventuallyEq (uncurry r0) (uncurry r1)
s : r0 x.1 x.2 = r1 x.1 x.2
⊢ s✝.bottcherNear x.1 ((f x.1)^[n] (r1 x.1 x.2)) = x.2 ^ d ^ n
Tactic:
simp only [← s, e.eqn]
State after:
no goals