internlm/Lean-Github huggingface dataset:
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
⊢ ∀ y ∈ insert a (Subtype.val '' s), m • y = y
Tactic:
intro x hx
Proof state after:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx : x ∈ insert a (Subtype.val '' s)
⊢ m • x = x
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx : x ∈ insert a (Subtype.val '' s)
⊢ m • x = x
Tactic:
cases' Set.mem_insert_iff.mp hx with hx hx
Proof state after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x = a
⊢ m • x = x

case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x ∈ Subtype.val '' s
⊢ m • x = x
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
this : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
⊢ ∃ a_1,
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := m, property := hm }, property := hm' }
Tactic:
use ⟨m, this⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
this : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
⊢ MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := this } =
    { val := { val := m, property := hm }, property := hm' }
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
this : m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
⊢ MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := this } =
    { val := { val := m, property := hm }, property := hm' }
Tactic:
rfl
Proof state after:
no goals
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x = a
⊢ m • x = x
Tactic:
rw [hx]
Proof state after:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x = a
⊢ m • a = a
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x = a
⊢ m • a = a
Tactic:
exact mem_stabilizer_iff.mp hm
Proof state after:
no goals
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
x : α
hx✝ : x ∈ insert a (Subtype.val '' s)
hx : x ∈ Subtype.val '' s
⊢ m • x = x
Tactic:
obtain ⟨y, hy, rfl⟩ := (Set.mem_image _ _ _).mp hx
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
⊢ m • ↑y = ↑y
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : { val := m, property := hm } ∈ fixingSubgroup (↥(stabilizer M a)) s
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
⊢ m • ↑y = ↑y
Tactic:
rw [mem_fixingSubgroup_iff] at hm'
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
⊢ m • ↑y = ↑y
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
⊢ m • ↑y = ↑y
Tactic:
let hz := hm' y hy
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
hz : { val := m, property := hm } • y = y := hm' y hy
⊢ m • ↑y = ↑y
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
hz : { val := m, property := hm } • y = y := hm' y hy
⊢ m • ↑y = ↑y
Tactic:
rw [← SetLike.coe_eq_coe, SubMulAction.val_smul_of_tower] at hz
Proof state after:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
hz : { val := m, property := hm } • ↑y = ↑y
⊢ m • ↑y = ↑y
Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective
Proof state before:
case right.mk.mk.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
m : M
hm : m ∈ stabilizer M a
hm' : ∀ y ∈ s, { val := m, property := hm } • y = y
y : ↥(ofStabilizer M a)
hy : y ∈ s
hx✝ : ↑y ∈ insert a (Subtype.val '' s)
hx : ↑y ∈ Subtype.val '' s
hz : { val := m, property := hm } • ↑y = ↑y
⊢ m • ↑y = ↑y
Tactic:
exact hz
Proof state after:
no goals
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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)
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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)
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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)
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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⟩
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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]
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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]
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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⟩
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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
Proof state after:
no goals
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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⟩
Proof 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)
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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⟩
Proof 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 }
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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]
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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]
Proof 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
Theorem: fixingSubgroup_smul_eq_fixingSubgroup_map_conj
Proof 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⟩
Proof state after:
no goals
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Bijective ⇑(conjMap_ofFixingSubgroup M hst)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Injective ⇑(conjMap_ofFixingSubgroup M hst)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Surjective ⇑(conjMap_ofFixingSubgroup M hst)
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Injective ⇑(conjMap_ofFixingSubgroup M hst)
Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Tactic:
simp only [Subtype.mk_eq_mk]
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { val := y, property := hy }
⊢ x = y
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  (conjMap_ofFixingSubgroup M hst) { val := x, property := hx } =
    (conjMap_ofFixingSubgroup M hst) { val := y, property := hy }
⊢ x = y
Tactic:
rw [← SetLike.coe_eq_coe] at hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  ↑((conjMap_ofFixingSubgroup M hst) { val := x, property := hx }) =
    ↑((conjMap_ofFixingSubgroup M hst) { val := y, property := hy })
⊢ x = y
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy :
  ↑((conjMap_ofFixingSubgroup M hst) { val := x, property := hx }) =
    ↑((conjMap_ofFixingSubgroup M hst) { val := y, property := hy })
⊢ x = y
Tactic:
change g • x = g • y at hxy
Proof state after:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : g • x = g • y
⊢ x = y
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M s
y : α
hy : y ∈ ofFixingSubgroup M s
hxy : g • x = g • y
⊢ x = y
Tactic:
apply (MulAction.injective g) hxy
Proof state after:
no goals
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Function.Surjective ⇑(conjMap_ofFixingSubgroup M hst)
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Tactic:
have hst' : g⁻¹ • t = s := by
  apply symm; rw [← inv_smul_eq_iff]; rw [inv_inv]
  exact hst
Proof state after:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Theorem: SubMulAction.conjMap_ofFixingSubgroup_bijective
Proof state before:
case right.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ ∃ a, (conjMap_ofFixingSubgroup M hst) a = { val := x, property := hx }
Tactic:
use (SubMulAction.conjMap_ofFixingSubgroup M hst') ⟨x, hx⟩
Proof state after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x : α
hx : x ∈ ofFixingSubgroup M t
hst' : g⁻¹ • t = s
⊢ (conjMap_ofFixingSubgroup M hst) ((conjMap_ofFixingSubgroup M hst') { val := x, property := hx }) =
    { val := x, property := hx }