case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)

case neg
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
by_cases hx : x ∈ periodicPts f
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
have hx' := minimalPeriod_pos_of_mem_periodicPts hx
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)) ↔
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
rw [periodicOrbit, ← Cycle.map_coe, Cycle.chain_map, ← hM, Cycle.chain_range_succ]
case pos.refine'_1
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)) →
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)

case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
case pos
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)) ↔
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
refine' ⟨_, fun H => ⟨_, fun m hm => H _ (hm.trans (Nat.lt_succ_self _))⟩⟩
case pos.refine'_1.intro
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
case pos.refine'_1
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x) ∧
      ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)) →
    ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
rintro ⟨hr, H⟩ n hn
case pos.refine'_1.intro.inl
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)

case pos.refine'_1.intro.inr
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
case pos.refine'_1.intro
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
cases' eq_or_lt_of_le (lt_succ_iff.1 hn) with hM' hM'
no goals
case pos.refine'_1.intro.inl
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
rwa [hM', hM, iterate_minimalPeriod]
no goals
case pos.refine'_1.intro.inr
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n✝ : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
H : ∀ (m : ℕ), m < minimalPeriod f x - succ 0 → r ((f^[m]) x) ((f^[succ m]) x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r ((f^[n]) x) ((f^[n + 1]) x)
exact H _ hM'
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) x
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[0]) x)
rw [iterate_zero_apply]
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[minimalPeriod f x]) x)
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) x
nth_rw 3 [← @iterate_minimalPeriod α f x]
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[minimalPeriod f x - succ 0 + succ 0]) x)
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[minimalPeriod f x]) x)
nth_rw 2 [← hM]
no goals
case pos.refine'_2
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ (n : ℕ), n < minimalPeriod f x - succ 0 + succ 0 → r ((f^[n]) x) ((f^[n + 1]) x)
⊢ r ((f^[minimalPeriod f x - succ 0]) x) ((f^[minimalPeriod f x - succ 0 + succ 0]) x)
exact H _ (Nat.lt_succ_self _)
case neg
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ (n : ℕ), n < 0 → r ((f^[n]) x) ((f^[n + 1]) x)
case neg
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), n < minimalPeriod f x → r ((f^[n]) x) ((f^[n + 1]) x)
rw [periodicOrbit_eq_nil_of_not_periodic_pt hx, minimalPeriod_eq_zero_of_nmem_periodicPts hx]
no goals
case neg
α : Type u_1
β : Type ?u.34705
f✝ fa : α → α
fb : β → β
x✝ y : α
m n : ℕ
r : α → α → Prop
f : α → α
x : α
hx : ¬x ∈ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ (n : ℕ), n < 0 → r ((f^[n]) x) ((f^[n + 1]) x)
simp