Theorem: SubMulAction.scalarMap_ofFixingSubgroupOfStabilizer_bijective (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Bijective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
constructor
State after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))

State before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Injective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
rintro ⟨m, hm⟩ ⟨n, hn⟩ hmn
State after:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm } =
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn }
⊢ { val := m, property := hm } = { val := n, property := hn }

State before:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm } =
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn }
⊢ { val := m, property := hm } = { val := n, property := hn }
Tactic:
rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe] at hmn
State after:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ { val := m, property := hm } = { val := n, property := hn }

State before:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ { val := m, property := hm } = { val := n, property := hn }
Tactic:
simp only [Subtype.mk_eq_mk]
State after:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ m = n

State before:
case left.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 ∈ fixingSubgroup M (insert a (Subtype.val '' s))
n : M
hn : n ∈ fixingSubgroup M (insert a (Subtype.val '' s))
hmn :
  ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := m, property := hm }) =
    ↑↑(MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) { val := n, property := hn })
⊢ m = n
Tactic:
exact hmn
State after:
no goals

State before:
case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
⊢ Function.Surjective (MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s))
Tactic:
rintro ⟨⟨m, hm⟩, hm'⟩
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
⊢ ∃ a_1,
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := m, property := hm }, property := hm' }

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
⊢ ∃ a_1,
    MulActionHom.toMap (equivariantMap_ofFixingSubgroup_to_ofStabilizer M a s) a_1 =
      { val := { val := m, property := hm }, property := hm' }
Tactic:
suffices m ∈ fixingSubgroup M (insert a (Subtype.val '' s)) by
  use ⟨m, this⟩
  rfl
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
⊢ m ∈ fixingSubgroup M (insert a (Subtype.val '' s))

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
⊢ m ∈ fixingSubgroup M (insert a (Subtype.val '' s))
Tactic:
rw [mem_fixingSubgroup_iff]
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
⊢ ∀ y ∈ insert a (Subtype.val '' s), m • y = y

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
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

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
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

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⟩
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' }

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
State after:
no goals

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]
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

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
State after:
no goals

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
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

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'
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

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
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

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
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

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
State after:
no goals