case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

case refine'_2
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
⊢ minimalPeriod f x = 1 ↔ IsFixedPt f x
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt (f^[1]) x
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt f x
rw [← iterate_one f]
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsFixedPt (f^[1]) x
refine' Function.IsPeriodicPt.isFixedPt _
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x
rw [← h]
no goals
case refine'_1
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x
exact isPeriodicPt_minimalPeriod f x
no goals
case refine'_2
α : Type u_1
β : Type ?u.25081
f fa : α → α
fb : β → β
x y : α
m n : ℕ
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
exact
  ((h.isPeriodicPt 1).minimalPeriod_le Nat.one_pos).antisymm
    (Nat.succ_le_of_lt ((h.isPeriodicPt 1).minimalPeriod_pos Nat.one_pos))