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

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

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

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • {a} = g' • {a} ∨ Disjoint (g • {a}) (g' • {a})
Tactic:
simp only [Set.smul_set_singleton, Set.singleton_eq_singleton_iff, Set.disjoint_singleton, Ne.def]
State after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • a = g' • a ∨ ¬g • a = g' • a

State before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • a = g' • a ∨ ¬g • a = g' • a
Tactic:
apply em
State after:
no goals