G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ (if h : ExponentExists G then Nat.find h else 0) ≠ 0
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ exponent G ≠ 0
rw [exponent]
case inl
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ ExponentExists G ↔ Nat.find h ≠ 0

case inr
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ ExponentExists G ↔ 0 ≠ 0
G : Type u
inst✝ : Monoid G
⊢ ExponentExists G ↔ (if h : ExponentExists G then Nat.find h else 0) ≠ 0
split_ifs with h
no goals
case inl
G : Type u
inst✝ : Monoid G
h : ExponentExists G
⊢ ExponentExists G ↔ Nat.find h ≠ 0
simp [h, @not_lt_zero' ℕ]
no goals
case inr
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
⊢ ExponentExists G ↔ 0 ≠ 0
tauto