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

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

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
Tactic:
intro h'
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : (MulEquiv.toMonoidHom (MulAut.conj g)) h = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : (MulEquiv.toMonoidHom (MulAut.conj g)) h = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ h' • g • B = g • h • B
Tactic:
suffices (h' : G) • g • B = g • h • B by
  rw [← this]; rfl
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B
Tactic:
rw [← hh]
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹) • g • B = g • h • B

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹) • g • B = g • h • B
Tactic:
rw [smul_smul (g * h * g⁻¹) g B]
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = g • h • B

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = g • h • B
Tactic:
rw [smul_smul g h B]
State after:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = (g * h) • B

State before:
case intro.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹ * g) • B = (g * h) • B
Tactic:
simp only [inv_mul_cancel_right]
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ h' • g • B = g • B ∨ Disjoint (h' • g • B) (g • B)
Tactic:
simp only [this]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
cases' IsBlock.def_one.mp hB ⟨h, hH⟩ with heq hdis
State after:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)

case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)

State before:
case inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
left
State after:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B

State before:
case inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
heq : { val := h, property := hH } • B = B
⊢ g • h • B = g • B
Tactic:
congr
State after:
no goals

State before:
case inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ g • h • B = g • B ∨ Disjoint (g • h • B) (g • B)
Tactic:
right
State after:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ Disjoint (g • h • B) (g • B)

State before:
case inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : h' • g • B = g • h • B
hdis : Disjoint ({ val := h, property := hH } • B) B
⊢ Disjoint (g • h • B) (g • B)
Tactic:
exact Set.disjoint_image_of_injective (MulAction.injective g) hdis
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = g • h • B
Tactic:
rw [← this]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
this : ↑h' • g • B = g • h • B
⊢ h' • g • B = ↑h' • g • B
Tactic:
rfl
State after:
no goals