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

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ IsBlock G ⊥
Tactic:
rw [IsBlock.def]
State after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ ∀ (g g' : G), g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ ∀ (g g' : G), g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Tactic:
intro g g'
State after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Tactic:
apply Or.intro_left
State after:
case h
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥

State before:
case h
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥
Tactic:
simp only [Set.bot_eq_empty, Set.smul_set_empty]
State after:
no goals