Theorem: MulAction.subsingleton_IsBlock (Jordan/Blocks.lean)

State before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
⊢ IsBlock G B
Tactic:
cases Set.Subsingleton.eq_empty_or_singleton hB with
| inl h => rw [h]; apply bot_IsBlock
| inr h => obtain ⟨a, ha⟩ := h; rw [ha]; apply singleton_IsBlock
State after:
no goals

State before:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G B
Tactic:
rw [h]
State after:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G ∅

State before:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G ∅
Tactic:
apply bot_IsBlock
State after:
no goals

State before:
case inr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : ∃ x, B = {x}
⊢ IsBlock G B
Tactic:
obtain ⟨a, ha⟩ := h
State after:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G B

State before:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G B
Tactic:
rw [ha]
State after:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G {a}

State before:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G {a}
Tactic:
apply singleton_IsBlock
State after:
no goals