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

State before:
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
⊢ Set.range f^[2] = Set.range f
Tactic:
rcases exists_iterate_idempotent f with ⟨n, h0, h1⟩
State after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ Set.range f^[2] = Set.range f

State before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ Set.range f^[2] = Set.range f
Tactic:
refine range_iter_two_eq_of_exists_iter_eq_self
  (Nat.lt_add_of_pos_left h0) (h _ ?_)
State after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1] ∘ f ∘ f^[n + 1]

State before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1] ∘ f ∘ f^[n + 1]
Tactic:
rw [← f.iterate_succ', ← f.iterate_add]
State after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1 + (n + 1).succ]

State before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ f ∘ f^[n + 1] ∘ f = f^[n + 1 + (n + 1).succ]
Tactic:
change (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]
State after:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]

State before:
case intro.intro
S : Type u_1
inst✝¹ : Fintype S
inst✝ : DecidableEq S
f : S → S
h : ∀ (g : S → S), f ∘ g ∘ f = g ∘ f ∘ g → g = f
n : ℕ
h0 : 0 < n
h1 : f^[2 * n] = f^[n]
⊢ (f ∘ f^[n]) ∘ f^[2] = f^[n + 1 + n] ∘ f^[2]
Tactic:
rw [Nat.succ_add, ← Nat.two_mul, f.iterate_succ' (2 * n), h1]
State after:
no goals