Theorem: aperiodic_next (meetings/ex4.lean)

State before:
⊢ Function.periodicPts next = ∅
Tactic:
simp_rw [Function.periodicPts, Function.IsPeriodicPt, Function.IsFixedPt]
State after:
⊢ {x | ∃ n > 0, next^[n] x = x} = ∅

State before:
⊢ {x | ∃ n > 0, next^[n] x = x} = ∅
Tactic:
ext x
State after:
case h
x : ℕ × ℕ
⊢ x ∈ {x | ∃ n > 0, next^[n] x = x} ↔ x ∈ ∅

State before:
case h
x : ℕ × ℕ
⊢ x ∈ {x | ∃ n > 0, next^[n] x = x} ↔ x ∈ ∅
Tactic:
simp only [gt_iff_lt, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_exists, not_and]
State after:
case h
x : ℕ × ℕ
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬next^[x_1] x = x

State before:
case h
x : ℕ × ℕ
⊢ ∀ (x_1 : ℕ), 0 < x_1 → ¬next^[x_1] x = x
Tactic:
intro n hlt heq
State after:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : next^[n] x = x
⊢ False

State before:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : next^[n] x = x
⊢ False
Tactic:
simp_rw [next_apply] at heq
State after:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x
⊢ False

State before:
case h
x : ℕ × ℕ
n : ℕ
hlt : 0 < n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x
⊢ False
Tactic:
induction' n with n ih
State after:
case h.zero
x : ℕ × ℕ
hlt : 0 < Nat.zero
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.zero] x = x
⊢ False

case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
hlt : 0 < Nat.succ n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.succ n] x = x
⊢ False

State before:
case h.zero
x : ℕ × ℕ
hlt : 0 < Nat.zero
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.zero] x = x
⊢ False
Tactic:
simp only [Nat.zero_eq, lt_self_iff_false] at hlt
State after:
no goals

State before:
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
hlt : 0 < Nat.succ n
heq : (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[Nat.succ n] x = x
⊢ False
Tactic:
simp at *
State after:
case h.succ
x : ℕ × ℕ
n : ℕ
ih : 0 < n → (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n] x = x → False
heq :
  (fun p => if p.1 = p.2 then (0, p.2 + 1) else (p.1 + 1, p.2))^[n]
      (if x.1 = x.2 then (0, x.2 + 1) else (x.1 + 1, x.2)) =
    x
hlt : True
⊢ False