α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ List.range (minimalPeriod f x) →
      ∀ (y : ℕ), y ∈ List.range (minimalPeriod f x) → (f^[x_1]) x = (f^[y]) x → x_1 = y
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ Cycle.Nodup (periodicOrbit f x)
rw [periodicOrbit, Cycle.nodup_coe_iff, List.nodup_map_iff_inj_on (List.nodup_range _)]
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : (f^[m]) x = (f^[n]) x
⊢ m = n
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ ∀ (x_1 : ℕ),
    x_1 ∈ List.range (minimalPeriod f x) →
      ∀ (y : ℕ), y ∈ List.range (minimalPeriod f x) → (f^[x_1]) x = (f^[y]) x → x_1 = y
intro m hm n hn hmn
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : (f^[m]) x = (f^[n]) x
⊢ m = n
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m ∈ List.range (minimalPeriod f x)
n : ℕ
hn : n ∈ List.range (minimalPeriod f x)
hmn : (f^[m]) x = (f^[n]) x
⊢ m = n
rw [List.mem_range] at hm hn
no goals
α : Type u_1
β : Type ?u.32137
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m : ℕ
hm : m < minimalPeriod f x
n : ℕ
hn : n < minimalPeriod f x
hmn : (f^[m]) x = (f^[n]) x
⊢ m = n
rwa [eq_iff_lt_minimalPeriod_of_iterate_eq hm hn] at hmn