Theorem: IMOSL.IMO2017A3.exists_iterate_idempotent (IMOSLLean4/IMO2017/A3/A3.lean)

State before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
obtain ⟨a, b, h, h0⟩ := exists_lt_iterate_eq f
State after:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a < b
h0 : f^[a] = f^[b]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]

State before:
case intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a b : ℕ
h : a < b
h0 : f^[a] = f^[b]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
rcases Nat.exists_eq_add_of_le h.le with ⟨c, rfl⟩
State after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : a < a + c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]

State before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : a < a + c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
rw [Nat.lt_add_right_iff_pos] at h
State after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]

State before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ ∃ n, 0 < n ∧ f^[2 * n] = f^[n]
Tactic:
refine ⟨c * a.succ, Nat.mul_pos h a.succ_pos, ?_⟩
State after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[2 * (c * a.succ)] = f^[c * a.succ]

State before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[2 * (c * a.succ)] = f^[c * a.succ]
Tactic:
rw [Nat.two_mul]
State after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c * a.succ] = f^[c * a.succ]

State before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c * a.succ] = f^[c * a.succ]
Tactic:
refine iterate_add_mul_eq ?_ _
State after:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c] = f^[c * a.succ]

State before:
case intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Tactic:
obtain ⟨k, h1⟩ := Nat.exists_eq_add_of_le
  (Nat.le_mul_of_pos_left a.succ h)
State after:
case intro.intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
k : ℕ
h1 : c * a.succ = a.succ + k
⊢ f^[c * a.succ + c] = f^[c * a.succ]

State before:
case intro.intro.intro.intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
a c : ℕ
h : 0 < c
h0 : f^[a] = f^[a + c]
k : ℕ
h1 : c * a.succ = a.succ + k
⊢ f^[c * a.succ + c] = f^[c * a.succ]
Tactic:
rw [h1, Nat.add_right_comm, f.iterate_add, Nat.succ_add,
  f.iterate_succ, ← h0, ← f.iterate_succ, f.iterate_add]
State after:
no goals