α : Type u_1
β : Type ?u.23726
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : (f^[m]) x = (f^[n]) x
hmn' : n < m
⊢ False
α : Type u_1
β : Type ?u.23726
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : (f^[m]) x = (f^[n]) x
⊢ m ≤ n
by_contra' hmn'
α : Type u_1
β : Type ?u.23726
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : (f^[m - n]) ((f^[n]) x) = (f^[n]) x
hmn' : n < m
⊢ False
α : Type u_1
β : Type ?u.23726
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : (f^[m]) x = (f^[n]) x
hmn' : n < m
⊢ False
rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn
no goals
α : Type u_1
β : Type ?u.23726
f fa : α → α
fb : β → β
x y : α
m✝ n✝ m n : ℕ
hm : m < minimalPeriod f x
hmn : (f^[m - n]) ((f^[n]) x) = (f^[n]) x
hmn' : n < m
⊢ False
exact
  ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
            (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
              (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
        (Nat.sub_le m n)).not_lt
    hm