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

State before:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f^[2] = Set.range f
Tactic:
apply (Set.range_comp_subset_range f f).antisymm
State after:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)

State before:
S : Type u_1
m : ℕ
f : S → S
h : 2 ≤ m
h0 : f^[m] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
State after:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)

State before:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range f ⊆ Set.range (f ∘ f)
Tactic:
nth_rw 1 [← h0, f.iterate_add]
State after:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range (f^[2] ∘ f^[k]) ⊆ Set.range (f ∘ f)

State before:
case intro
S : Type u_1
f : S → S
k : ℕ
h : 2 ≤ 2 + k
h0 : f^[2 + k] = f
⊢ Set.range (f^[2] ∘ f^[k]) ⊆ Set.range (f ∘ f)
Tactic:
exact Set.range_comp_subset_range _ _
State after:
no goals