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

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

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

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

State before:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
g g' : G
⊢ g • B = g' • B
Tactic:
rw [hfB g, hfB g']
State after:
no goals