case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime (orderOf y) m
hg : orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y

case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime (orderOf y) m
hg : ¬orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
h : coprime (orderOf y) m
⊢ orderOf (y ^ m) = orderOf y
by_cases hg : orderOf y = 0
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 : coprime (orderOf y) m
hg : orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y
rw [m.coprime_zero_left.mp (hg ▸ h), pow_one]
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 : coprime (orderOf y) m
hg : ¬orderOf y = 0
⊢ orderOf (y ^ m) = orderOf y
rw [orderOf_pow'' y m (hg.imp_symm orderOf_eq_zero), h.gcd_eq_one, Nat.div_one]