G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False
G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
⊢ ¬IsSolvable (Perm X)
intro h
G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False
G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False
have key : Nonempty (Fin 5 ↪ X) := by
  rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
no goals
G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False
exact
  Equiv.Perm.fin_5_not_solvable
    (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))
no goals
G : Type ?u.94765
G' : Type ?u.94768
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_1
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ Nonempty (Fin 5 ↪ X)
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]