case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))

case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
by_cases h0 : orderOf x = 0
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ pred (orderOf x) * (x * y)) ∣ lcm (orderOf x) (orderOf (x * y))
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
conv_lhs =>
  rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
    _root_.pow_succ', mul_assoc]
no goals
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : ¬orderOf x = 0
⊢ orderOf (x ^ pred (orderOf x) * (x * y)) ∣ lcm (orderOf x) (orderOf (x * y))
exact
  (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
    (lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (dvd_lcm_left _ _), dvd_lcm_right _ _⟩)
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ lcm (orderOf x) (orderOf (x * y))
rw [h0, lcm_zero_left]
no goals
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : _root_.Commute x y
h0 : orderOf x = 0
⊢ orderOf y ∣ 0
apply dvd_zero