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

State before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ IsBlock H (⇑j ⁻¹' B)
Tactic:
rw [IsBlock.def_one]
State after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ ∀ (g : H), g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

State before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ ∀ (g : H), g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
intro g
State after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

State before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
cases' IsBlock.def_one.mp hB (φ g) with heq hdis
State after:
case inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

case inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

State before:
case inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
apply Or.intro_left
State after:
case inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B

State before:
case inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B
Tactic:
rw [← Set.preimage_smul_setₑ, heq]
State after:
no goals

State before:
case inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
apply Or.intro_right
State after:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

State before:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
rw [← Set.preimage_smul_setₑ]
State after:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)

State before:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)
Tactic:
apply Disjoint.preimage
State after:
case inr.h.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (φ g • B) B

State before:
case inr.h.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (φ g • B) B
Tactic:
exact hdis
State after:
no goals