Theorem: iterate_monotone_eq_zero (meetings/ex4.lean)

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
⊢ f^[n] x = x → n = 0
Tactic:
intro eq
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : Function.periodicPts f = ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
simp_rw [Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt] at hper
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : {x | ∃ n > 0, f^[n] x = x} = ∅
eq : f^[n] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : {x | ∃ n > 0, f^[n] x = x} = ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
rw [Set.ext_iff] at hper
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : ∀ (x : α), x ∈ {x | ∃ n > 0, f^[n] x = x} ↔ x ∈ ∅
eq : f^[n] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
hper : ∀ (x : α), x ∈ {x | ∃ n > 0, f^[n] x = x} ↔ x ∈ ∅
eq : f^[n] x = x
⊢ n = 0
Tactic:
simp at hper
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x : α) (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x : α) (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Tactic:
specialize hper x
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : ∀ (x_1 : ℕ), 0 < x_1 → ¬f^[x_1] x = x
⊢ n = 0
Tactic:
specialize hper n
State after:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
⊢ n = 0

State before:
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
⊢ n = 0
Tactic:
by_cases h : 0 < n
State after:
case pos
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : 0 < n
⊢ n = 0

case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0

State before:
case pos
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : 0 < n
⊢ n = 0
Tactic:
exact absurd eq (hper h)
State after:
no goals

State before:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : ¬0 < n
⊢ n = 0
Tactic:
simp only [not_lt, nonpos_iff_eq_zero] at h
State after:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : n = 0
⊢ n = 0

State before:
case neg
α : Type
inst✝ : Preorder α
f : α → α
x : α
n : ℕ
eq : f^[n] x = x
hper : 0 < n → ¬f^[n] x = x
h : n = 0
⊢ n = 0
Tactic:
exact h
State after:
no goals