Theorem: enumerator_bijective (meetings/ex4.lean)

State before:
⊢ Function.Bijective enumerator
Tactic:
simp_rw [Function.Bijective, enumerator_apply]
State after:
⊢ (Function.Injective fun n => next^[n] (0, 0)) ∧ Function.Surjective fun n => next^[n] (0, 0)

State before:
⊢ (Function.Injective fun n => next^[n] (0, 0)) ∧ Function.Surjective fun n => next^[n] (0, 0)
Tactic:
constructor
State after:
case left

⊢ Function.Injective fun n => next^[n] (0, 0)

case right

⊢ Function.Surjective fun n => next^[n] (0, 0)

State before:
case left

⊢ Function.Injective fun n => next^[n] (0, 0)
Tactic:
intros a b heq
State after:
case left
a b : ℕ
heq : (fun n => next^[n] (0, 0)) a = (fun n => next^[n] (0, 0)) b
⊢ a = b

State before:
case left
a b : ℕ
heq : (fun n => next^[n] (0, 0)) a = (fun n => next^[n] (0, 0)) b
⊢ a = b
Tactic:
simp only at heq
State after:
case left
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a = b

State before:
case left
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a = b
Tactic:
rw [Function.iterate_eq_iterate_iff_of_lt_minimalPeriod] at heq
State after:
case left
a b : ℕ
heq : a = b
⊢ a = b

case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < Function.minimalPeriod next (0, 0)

case left.hn
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ b < Function.minimalPeriod next (0, 0)

State before:
case left
a b : ℕ
heq : a = b
⊢ a = b
Tactic:
exact heq
State after:
no goals

State before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < Function.minimalPeriod next (0, 0)
Tactic:
rw [Function.minimalPeriod]
State after:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < if h : (0, 0) ∈ Function.periodicPts next then Nat.find h else 0

State before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a < if h : (0, 0) ∈ Function.periodicPts next then Nat.find h else 0
Tactic:
simp
State after:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a <
    if h : (0, 0) ∈ Function.periodicPts next then
      Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
    else 0

State before:
case left.hm
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
⊢ a <
    if h : (0, 0) ∈ Function.periodicPts next then
      Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
    else 0
Tactic:
split
State after:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ a < Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)

case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
⊢ a < 0

State before:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ a < Nat.find (_ : ∃ n, (fun n => 0 < n ∧ Function.IsPeriodicPt next n (0, 0)) n)
Tactic:
rw [Nat.lt_find_iff sorry a]
State after:
case left.hm.inl
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∈ Function.periodicPts next
⊢ ∀ m ≤ a, ¬(0 < m ∧ Function.IsPeriodicPt next m (0, 0))

State before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
⊢ a < 0
Tactic:
have foo := Function.iterate_cancel sorry heq
State after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : next^[a - b] (0, 0) = (0, 0)
⊢ a < 0

State before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : next^[a - b] (0, 0) = (0, 0)
⊢ a < 0
Tactic:
rw [←Function.IsFixedPt] at foo
State after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsFixedPt next^[a - b] (0, 0)
⊢ a < 0

State before:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsFixedPt next^[a - b] (0, 0)
⊢ a < 0
Tactic:
rw [←Function.IsPeriodicPt] at foo
State after:
case left.hm.inr
a b : ℕ
heq : next^[a] (0, 0) = next^[b] (0, 0)
h✝ : (0, 0) ∉ Function.periodicPts next
foo : Function.IsPeriodicPt next (a - b) (0, 0)
⊢ a < 0