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

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock G B
⊢ IsBlock G (g • B)
Tactic:
rw [IsBlock.of_top_iff] at hB ⊢
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)
Tactic:
suffices Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤ by
  rw [← this]
  exact IsBlock.of_subgroup_of_conjugate hB g
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
Tactic:
suffices ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ by
  rw [this]
  refine Subgroup.map_comap_eq_self_of_surjective ?_ _
  exact MulEquiv.surjective (MulAut.conj g)
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Tactic:
rw [Subgroup.comap_top]
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥⊤) (g • B)
Tactic:
rw [← this]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤)) (g • B)

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤)) (g • B)
Tactic:
exact IsBlock.of_subgroup_of_conjugate hB g
State after:
no goals

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤ = ⊤
Tactic:
rw [this]
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤) =
    Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤) =
    Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
Tactic:
refine Subgroup.map_comap_eq_self_of_surjective ?_ _
State after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom (MulAut.conj g))

State before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
this : ⊤ = Subgroup.comap (MulEquiv.toMonoidHom (MulAut.conj g)) ⊤
⊢ Function.Surjective ⇑(MulEquiv.toMonoidHom (MulAut.conj g))
Tactic:
exact MulEquiv.surjective (MulAut.conj g)
State after:
no goals