no goals
α : Type u_1
β : Type ?u.27026
f fa : α → α
fb : β → β
x y : α
m n p k : ℕ
hp : Fact (Nat.Prime p)
hk : ¬IsPeriodicPt f (p ^ k) x
hk1 : IsPeriodicPt f (p ^ (k + 1)) x
⊢ minimalPeriod f x = p ^ (k + 1)
apply Nat.eq_prime_pow_of_dvd_least_prime_pow hp.out <;>
  rwa [← isPeriodicPt_iff_minimalPeriod_dvd]