Theorem: eq_bot_iff_card (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:
constructor
State after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1

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

State before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∀ x ∈ H, x = 1) → ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
intro h
State after:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x

State before:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
h : ∀ x ∈ H, x = 1
⊢ ∃ x ∈ H, ∀ a ∈ H, a = x
Tactic:
use 1, H.one_mem
State after:
no goals

State before:
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
⊢ (∃ x ∈ H, ∀ a ∈ H, a = x) → ∀ x ∈ H, x = 1
Tactic:
rintro ⟨y, -, hy'⟩ x hx
State after:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1

State before:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Fintype ↥H
y : G
hy' : ∀ a ∈ H, a = y
x : G
hx : x ∈ H
⊢ x = 1
Tactic:
calc x = y := hy' x hx
_      = 1 := (hy' 1 H.one_mem).symm
State after:
no goals