Theorem: MulAction.IsBlock_image (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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ IsBlock H (⇑j '' B)
Tactic:
rw [IsBlock.def]
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ ∀ (g g' : H), g • ⇑j '' B = g' • ⇑j '' B ∨ Disjoint (g • ⇑j '' B) (g' • ⇑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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ ∀ (g g' : H), g • ⇑j '' B = g' • ⇑j '' B ∨ Disjoint (g • ⇑j '' B) (g' • ⇑j '' B)
Tactic:
intro h h'
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h h' : H
⊢ h • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (h • ⇑j '' B) (h' • ⇑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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h h' : H
⊢ h • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (h • ⇑j '' B) (h' • ⇑j '' B)
Tactic:
obtain ⟨g, rfl⟩ := hφ h
State after:
case intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h' : H
g : G
⊢ φ g • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (h' • ⇑j '' B)

State before:
case intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h' : H
g : G
⊢ φ g • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (h' • ⇑j '' B)
Tactic:
obtain ⟨g', rfl⟩ := hφ h'
State after:
case intro.intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ φ g • ⇑j '' B = φ g' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (φ g' • ⇑j '' B)

State before:
case intro.intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ φ g • ⇑j '' B = φ g' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (φ g' • ⇑j '' B)
Tactic:
simp only [← Set.image_smul_setₑ]
State after:
case intro.intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))

State before:
case intro.intro
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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
cases' IsBlock.def.mp hB g g' with h h
State after:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))

case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))

State before:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
apply Or.intro_left
State after:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B)

State before:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B)
Tactic:
rw [h]
State after:
no goals

State before:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
apply Or.intro_right
State after:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))

State before:
case intro.intro.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
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
exact Set.disjoint_image_of_injective hj h
State after:
no goals