Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
⊢ fixingSubgroup M (g • s) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)
Tactic:
ext h
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ fixingSubgroup M (g • s) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ fixingSubgroup M (g • s) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)
Tactic:
constructor
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ fixingSubgroup M (g • s) → h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)

case h.mpr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s) → h ∈ fixingSubgroup M (g • s)

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ fixingSubgroup M (g • s) → h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)
Tactic:
intro hh
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s)
Tactic:
use (MulAut.conj g⁻¹) h
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ (MulAut.conj g⁻¹) h ∈ ↑(fixingSubgroup M s) ∧ (MulEquiv.toMonoidHom (MulAut.conj g)) ((MulAut.conj g⁻¹) h) = h

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ (MulAut.conj g⁻¹) h ∈ ↑(fixingSubgroup M s) ∧ (MulEquiv.toMonoidHom (MulAut.conj g)) ((MulAut.conj g⁻¹) h) = h
Tactic:
simp
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * h * g ∈ fixingSubgroup M s ∧ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * h * g ∈ fixingSubgroup M s ∧ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
constructor
State after:
case h.left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * h * g ∈ fixingSubgroup M s

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h.left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * h * g ∈ fixingSubgroup M s

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
rintro ⟨x, hx⟩
State after:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ (g⁻¹ * h * g) • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ (g⁻¹ * h * g) • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
simp only [Subtype.coe_mk, ← smul_smul]
State after:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ g⁻¹ • h • g • x = x

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ g⁻¹ • h • g • x = x

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
rw [inv_smul_eq_iff]
State after:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ h • g • x = g • x

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h.left.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
x : α
hx : x ∈ s
⊢ h • g • x = g • x

case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
simpa only [Subtype.coe_mk] using hh ⟨_, Set.smul_mem_smul_set hx⟩
State after:
case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h

State before:
case h.right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
hh : h ∈ fixingSubgroup M (g • s)
⊢ g⁻¹ * (g * h * g⁻¹) * g = h
Tactic:
group
State after:
no goals

State before:
case h.mpr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
h : M
⊢ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (fixingSubgroup M s) → h ∈ fixingSubgroup M (g • s)
Tactic:
rintro ⟨k, hk, rfl⟩
State after:
case h.mpr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
⊢ (MulEquiv.toMonoidHom (MulAut.conj g)) k ∈ fixingSubgroup M (g • s)

State before:
case h.mpr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
⊢ (MulEquiv.toMonoidHom (MulAut.conj g)) k ∈ fixingSubgroup M (g • s)
Tactic:
rintro ⟨x, hx⟩
State after:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ (MulEquiv.toMonoidHom (MulAut.conj g)) k • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }

State before:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ (MulEquiv.toMonoidHom (MulAut.conj g)) k • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }
Tactic:
simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply, Subtype.coe_mk, ← smul_smul]
State after:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ g • k • g⁻¹ • x = x

State before:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ g • k • g⁻¹ • x = x
Tactic:
rw [smul_eq_iff_eq_inv_smul]
State after:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ k • g⁻¹ • x = g⁻¹ • x

State before:
case h.mpr.intro.intro.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
g : M
s : Set α
k : M
hk : k ∈ ↑(fixingSubgroup M s)
x : α
hx : x ∈ g • s
⊢ k • g⁻¹ • x = g⁻¹ • x
Tactic:
exact hk ⟨_, Set.mem_smul_set_iff_inv_smul_mem.mp hx⟩
State after:
no goals