α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x
apply h.minimalPeriod_of_comp_dvd_mul.antisymm
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
this :
  ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x

case this
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
suffices :
  ∀ {f g : α → α},
    Commute f g →
      coprime (minimalPeriod f x) (minimalPeriod g x) →
        minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
case this
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
case this
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
intro f g h hco
case this.refine'_1
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

case this.refine'_2
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
case this
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
refine' hco.dvd_of_dvd_mul_left (IsPeriodicPt.left_of_comp h _ _).minimalPeriod_dvd
no goals
α : Type u_1
β : Type ?u.27755
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
this :
  ∀ {f g : α → α},
    Commute f g → coprime (minimalPeriod f x) (minimalPeriod g x) → minimalPeriod f x ∣ minimalPeriod (f ∘ g) x
⊢ minimalPeriod f x * minimalPeriod g x ∣ minimalPeriod (f ∘ g) x
exact hco.mul_dvd_of_dvd_of_dvd (this h hco) (h.comp_eq.symm ▸ this h.symm hco.symm)
no goals
case this.refine'_1
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
exact (isPeriodicPt_minimalPeriod _ _).const_mul _
no goals
case this.refine'_2
α : Type u_1
β : Type ?u.27755
f✝ fa : α → α
fb : β → β
x y : α
m n : ℕ
g✝ : α → α
h✝ : Commute f✝ g✝
hco✝ : coprime (minimalPeriod f✝ x) (minimalPeriod g✝ x)
f g : α → α
h : Commute f g
hco : coprime (minimalPeriod f x) (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
exact (isPeriodicPt_minimalPeriod _ _).mul_const _