G✝ : Type ?u.40798
G' : Type ?u.40801
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_1
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
G✝ : Type ?u.40798
G' : Type ?u.40801
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_1
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G
letI hG' : CommGroup G := { hG with mul_comm := h }
case mk
G✝ : Type ?u.40798
G' : Type ?u.40801
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_1
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
G✝ : Type ?u.40798
G' : Type ?u.40801
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_1
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
cases hG
no goals
case mk
G✝ : Type ?u.40798
G' : Type ?u.40801
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_1
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
exact CommGroup.isSolvable