Theorem: eq_bot_iff_card (LeanCourse/MIL/C08_Groups_and_Rings/S01_Groups.lean)

State before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ H = ⊥ ↔ card (↥H) = 1
Tactic:
suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
  simpa [eq_bot_iff_forall, card_eq_one_iff]
State after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x

State before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
⊢ (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
sorry
State after:
no goals

State before:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype (↥H)
this : (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x
⊢ H = ⊥ ↔ card (↥H) = 1
Tactic:
simpa [eq_bot_iff_forall, card_eq_one_iff]
State after:
no goals