Theorem: Super.isNiceN_mono (Ray/Dynamics/Potential.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 : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
⊢ s.IsNiceN c p n1
Tactic:
intro z zp
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 : ℕ
s : Super f d a
c : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

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 : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
rcases nice z zp with ⟨m, nc⟩
State after:
case intro
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 : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
m : (c, (f c)^[n0] z) ∈ s.near
nc : ∀ (k : ℕ), n0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

State before:
case intro
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 : ℂ
p : ℝ
n0 n1 : ℕ
nice : s.IsNiceN c p n0
n01 : n0 ≤ n1
z : S
zp : s.potential c z ≤ p
m : (c, (f c)^[n0] z) ∈ s.near
nc : ∀ (k : ℕ), n0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ (c, (f c)^[n1] z) ∈ s.near ∧ ∀ (k : ℕ), n1 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
use s.iter_stays_near' m n01, fun k n1k ↦ nc k (_root_.trans n01 n1k)
State after:
no goals