-- Mathlib/Dynamics/PeriodicPts/Lemmas.lean
theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Commute f g)
    (hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
    minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Proof state:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x

Tactic:
suffices
  ∀ {f g : α → α},
    Commute f g →
      Coprime (minimalPeriod f x) (minimalPeriod g x) →
        minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from
  hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)

Result:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Proof state:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Function.Commute f g → (minimalPeriod f x).Coprime (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
intro f g h hco

Result:
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Proof state:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x

Tactic:
apply h.minimalPeriod_of_comp_dvd_mul.antisymm

Result:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x

Proof state:
case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).const_mul _

Result:
no goals

Proof state:
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x

Tactic:
refine hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h ?_ ?_).minimalPeriod_dvd

Result:
case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Proof state:
case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
exact (isPeriodicPt_minimalPeriod _ _).mul_const _

Result:
no goals