Theorem: Eqn.mono (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 : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ s.bottcherNear x.1 ((f x.1)^[m] (r x.1 x.2)) = x.2 ^ d ^ m
Tactic:
refine Nat.le_induction e.eqn ?_ m nm
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 : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ ∀ (n_1 : ℕ),
    n ≤ n_1 →
      s.bottcherNear x.1 ((f x.1)^[n_1] (r x.1 x.2)) = x.2 ^ d ^ n_1 →
        s.bottcherNear x.1 ((f x.1)^[n_1 + 1] (r x.1 x.2)) = x.2 ^ d ^ (n_1 + 1)

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 : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
⊢ ∀ (n_1 : ℕ),
    n ≤ n_1 →
      s.bottcherNear x.1 ((f x.1)^[n_1] (r x.1 x.2)) = x.2 ^ d ^ n_1 →
        s.bottcherNear x.1 ((f x.1)^[n_1 + 1] (r x.1 x.2)) = x.2 ^ d ^ (n_1 + 1)
Tactic:
intro k nk h
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 : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
k : ℕ
nk : n ≤ k
h : s.bottcherNear x.1 ((f x.1)^[k] (r x.1 x.2)) = x.2 ^ d ^ k
⊢ s.bottcherNear x.1 ((f x.1)^[k + 1] (r x.1 x.2)) = x.2 ^ d ^ (k + 1)

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 : ℂ × ℂ
e : Eqn s n r x
m : ℕ
nm : n ≤ m
k : ℕ
nk : n ≤ k
h : s.bottcherNear x.1 ((f x.1)^[k] (r x.1 x.2)) = x.2 ^ d ^ k
⊢ s.bottcherNear x.1 ((f x.1)^[k + 1] (r x.1 x.2)) = x.2 ^ d ^ (k + 1)
Tactic:
simp only [h, Function.iterate_succ_apply',
  s.bottcherNear_eqn (s.iter_stays_near' e.near nk), pow_succ, pow_mul]
State after:
no goals