case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G ≤ 1

case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 1 ≤ exponent G
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G = 1
apply le_antisymm
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ exponent G ≤ 1
apply exponent_min' _ Nat.one_pos
no goals
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
simp
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 0 < exponent G
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 1 ≤ exponent G
apply Nat.succ_le_of_lt
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ 0 < exponent G
apply exponent_pos_of_exists 1 Nat.one_pos
no goals
case a.h
G : Type u
inst✝¹ : Monoid G
inst✝ : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
simp