Theorem: fixingSubgroup_of_insert (Jordan/SubMulActions.lean)

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
⊢ fixingSubgroup M (insert a ((fun x => ↑x) '' s)) =
    Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)
Tactic:
ext m
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s)) ↔
    m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s)) ↔
    m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)
Tactic:
constructor
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s)) →
    m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)

case h.mpr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) →
    m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s)) →
    m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)
Tactic:
intro hm
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)
Tactic:
rw [mem_fixingSubgroup_iff] at hm
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s)
Tactic:
rw [Subgroup.mem_map]
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ ∃ x ∈ fixingSubgroup (↥(stabilizer M a)) s, (Subgroup.subtype (stabilizer M a)) x = m

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ ∃ x ∈ fixingSubgroup (↥(stabilizer M a)) s, (Subgroup.subtype (stabilizer M a)) x = m
Tactic:
suffices hm' : m ∈ stabilizer M a by
  use ⟨m, hm'⟩
  simp only [Subgroup.coeSubtype, and_true]
  rw [mem_fixingSubgroup_iff]
  rintro ⟨y, hy⟩ hy'
  simp only [SetLike.mk_smul_mk, Subtype.mk.injEq]
  change m • y = y
  apply hm
  apply Set.mem_insert_of_mem
  use ⟨y, hy⟩
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m ∈ stabilizer M a

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m ∈ stabilizer M a
Tactic:
simp only [mem_stabilizer_iff]
State after:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m • a = a

State before:
case h.mp
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ m • a = a
Tactic:
apply hm
State after:
case h.mp.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ a ∈ insert a ((fun x => ↑x) '' s)

State before:
case h.mp.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
⊢ a ∈ insert a ((fun x => ↑x) '' s)
Tactic:
apply Set.mem_insert a
State after:
no goals

State before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ ∃ x ∈ fixingSubgroup (↥(stabilizer M a)) s, (Subgroup.subtype (stabilizer M a)) x = m
Tactic:
use ⟨m, hm'⟩
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ { val := m, property := hm' } ∈ fixingSubgroup (↥(stabilizer M a)) s ∧
    (Subgroup.subtype (stabilizer M a)) { val := m, property := hm' } = m

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ { val := m, property := hm' } ∈ fixingSubgroup (↥(stabilizer M a)) s ∧
    (Subgroup.subtype (stabilizer M a)) { val := m, property := hm' } = m
Tactic:
simp only [Subgroup.coeSubtype, and_true]
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ { val := m, property := hm' } ∈ fixingSubgroup (↥(stabilizer M a)) s

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ { val := m, property := hm' } ∈ fixingSubgroup (↥(stabilizer M a)) s
Tactic:
rw [mem_fixingSubgroup_iff]
State after:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ ∀ y ∈ s, { val := m, property := hm' } • y = y

State before:
case h
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
⊢ ∀ y ∈ s, { val := m, property := hm' } • y = y
Tactic:
rintro ⟨y, hy⟩ hy'
State after:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ { val := m, property := hm' } • { val := y, property := hy } = { val := y, property := hy }

State before:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ { val := m, property := hm' } • { val := y, property := hy } = { val := y, property := hy }
Tactic:
simp only [SetLike.mk_smul_mk, Subtype.mk.injEq]
State after:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ { val := m, property := hm' } • y = y

State before:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ { val := m, property := hm' } • y = y
Tactic:
change m • y = y
State after:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ m • y = y

State before:
case h.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ m • y = y
Tactic:
apply hm
State after:
case h.mk.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ y ∈ insert a ((fun x => ↑x) '' s)

State before:
case h.mk.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ y ∈ insert a ((fun x => ↑x) '' s)
Tactic:
apply Set.mem_insert_of_mem
State after:
case h.mk.a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ y ∈ (fun x => ↑x) '' s

State before:
case h.mk.a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
hm : ∀ y ∈ insert a ((fun x => ↑x) '' s), m • y = y
hm' : m ∈ stabilizer M a
y : α
hy : y ∈ SubMulAction.ofStabilizer M a
hy' : { val := y, property := hy } ∈ s
⊢ y ∈ (fun x => ↑x) '' s
Tactic:
use ⟨y, hy⟩
State after:
no goals

State before:
case h.mpr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
m : M
⊢ m ∈ Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) s) →
    m ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))
Tactic:
rintro ⟨⟨n, hn'⟩, hn, rfl⟩
State after:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : { val := n, property := hn' } ∈ ↑(fixingSubgroup (↥(stabilizer M a)) s)
⊢ (Subgroup.subtype (stabilizer M a)) { val := n, property := hn' } ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))

State before:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : { val := n, property := hn' } ∈ ↑(fixingSubgroup (↥(stabilizer M a)) s)
⊢ (Subgroup.subtype (stabilizer M a)) { val := n, property := hn' } ∈ fixingSubgroup M (insert a ((fun x => ↑x) '' s))
Tactic:
simp only [Subgroup.coeSubtype, SetLike.mem_coe, mem_fixingSubgroup_iff] at hn ⊢
State after:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
⊢ ∀ y ∈ insert a ((fun x => ↑x) '' s), n • y = y

State before:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
⊢ ∀ y ∈ insert a ((fun x => ↑x) '' s), n • y = y
Tactic:
intro x hx
State after:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ insert a ((fun x => ↑x) '' s)
⊢ n • x = x

State before:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ insert a ((fun x => ↑x) '' s)
⊢ n • x = x
Tactic:
rw [Set.mem_insert_iff] at hx
State after:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x = a ∨ x ∈ (fun x => ↑x) '' s
⊢ n • x = x

State before:
case h.mpr.intro.mk.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x = a ∨ x ∈ (fun x => ↑x) '' s
⊢ n • x = x
Tactic:
cases' hx with hx hx
State after:
case h.mpr.intro.mk.intro.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x = a
⊢ n • x = x

case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ (fun x => ↑x) '' s
⊢ n • x = x

State before:
case h.mpr.intro.mk.intro.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x = a
⊢ n • x = x

case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ (fun x => ↑x) '' s
⊢ n • x = x
Tactic:
. simpa [hx] using hn'
State after:
case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ (fun x => ↑x) '' s
⊢ n • x = x

State before:
case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ (fun x => ↑x) '' s
⊢ n • x = x
Tactic:
. simp only [Set.mem_image] at hx
  rcases hx with ⟨y, hy, rfl⟩
  conv_rhs => rw [← hn y hy]
State after:
no goals

State before:
case h.mpr.intro.mk.intro.inl
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x = a
⊢ n • x = x
Tactic:
simpa [hx] using hn'
State after:
no goals

State before:
case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : x ∈ (fun x => ↑x) '' s
⊢ n • x = x
Tactic:
simp only [Set.mem_image] at hx
State after:
case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : ∃ x_1 ∈ s, ↑x_1 = x
⊢ n • x = x

State before:
case h.mpr.intro.mk.intro.inr
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
x : α
hx : ∃ x_1 ∈ s, ↑x_1 = x
⊢ n • x = x
Tactic:
rcases hx with ⟨y, hy, rfl⟩
State after:
case h.mpr.intro.mk.intro.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ s
⊢ n • ↑y = ↑y

State before:
case h.mpr.intro.mk.intro.inr.intro.intro
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
s : Set ↥(SubMulAction.ofStabilizer M a)
n : M
hn' : n ∈ stabilizer M a
hn : ∀ y ∈ s, { val := n, property := hn' } • y = y
y : ↥(SubMulAction.ofStabilizer M a)
hy : y ∈ s
⊢ n • ↑y = ↑y
Tactic:
conv_rhs => rw [← hn y hy]
State after:
no goals