case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1

case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
G : Type u
inst✝ : Monoid G
g : G
⊢ g ^ exponent G = 1
by_cases ExponentExists G
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ exponent G = 1
simp_rw [exponent, dif_pos h]
no goals
case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1
exact (Nat.find_spec h).2 g
no goals
case neg
G : Type u
inst✝ : Monoid G
g : G
h : ¬ExponentExists G
⊢ g ^ exponent G = 1
simp_rw [exponent, dif_neg h, pow_zero]