Theorem: MulAction.Subgroup.IsBlock (Jordan/Blocks.lean)

State before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ MulAction.IsBlock (↥H) B
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ ∀ (g : ↥H), g • B = B ∨ Disjoint (g • B) B

State before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ ∀ (g : ↥H), g • B = B ∨ Disjoint (g • B) B
Tactic:
rintro ⟨g, _⟩
State after:
case mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
g : G
property✝ : g ∈ H
⊢ { val := g, property := property✝ } • B = B ∨ Disjoint ({ val := g, property := property✝ } • B) B

State before:
case mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
g : G
property✝ : g ∈ H
⊢ { val := g, property := property✝ } • B = B ∨ Disjoint ({ val := g, property := property✝ } • B) B
Tactic:
simpa only using IsBlock.def_one.mp hfB g
State after:
no goals