Theorem: IsPreprimitive.has_trivial_blocks (Jordan/Primitive.lean)

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ Set.Subsingleton B ∨ B = ⊤
Tactic:
apply h.has_trivial_blocks'
State after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ IsBlock G B

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ IsBlock G B
Tactic:
exact hB
State after:
no goals