G : Type u_1
inst✝³ : Group G
A : Type ?u.12172
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ H = ⊤
G : Type u_1
inst✝³ : Group G
A : Type ?u.12172
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
⊢ H = ⊤
letI : Fintype (H : Set G) := ‹Fintype H›
G : Type u_1
inst✝³ : Group G
A : Type ?u.12172
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ Fintype.card ↑↑H = Fintype.card { x // x ∈ H }
G : Type u_1
inst✝³ : Group G
A : Type ?u.12172
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ H = ⊤
rw [SetLike.ext'_iff, coe_top, ← Finset.coe_univ, ← (H : Set G).coe_toFinset, Finset.coe_inj, ←
  Finset.card_eq_iff_eq_univ, ← h, Set.toFinset_card]
no goals
G : Type u_1
inst✝³ : Group G
A : Type ?u.12172
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ Fintype.card ↑↑H = Fintype.card { x // x ∈ H }
congr