internlm/Lean-Github huggingface dataset:
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + PartENat.card ↥(ofStabilizer M a) = PartENat.card α
Tactic:
unfold PartENat.card
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) = Cardinal.toPartENat (Cardinal.mk α)
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) = Cardinal.toPartENat (Cardinal.mk α)
Tactic:
rw [← Cardinal.mk_sum_compl {a}, map_add]
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) =
    Cardinal.toPartENat (Cardinal.mk ↑{a}) + Cardinal.toPartENat (Cardinal.mk ↑{a}ᶜ)
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 + Cardinal.toPartENat (Cardinal.mk ↥(ofStabilizer M a)) =
    Cardinal.toPartENat (Cardinal.mk ↑{a}) + Cardinal.toPartENat (Cardinal.mk ↑{a}ᶜ)
Tactic:
congr
Proof state after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat (Cardinal.mk ↑{a})
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat (Cardinal.mk ↑{a})
Tactic:
simp only [Cardinal.mk_fintype, Fintype.card_ofSubsingleton, Nat.cast_one]
Proof state after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat 1
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ 1 = Cardinal.toPartENat 1
Tactic:
conv_lhs => rw [← Nat.cast_one]
Proof state after:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ ↑1 = Cardinal.toPartENat 1
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
case e_a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ ↑1 = Cardinal.toPartENat 1
Tactic:
apply symm
Proof state after:
case e_a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Cardinal.toPartENat 1 = ↑1
Theorem: SubMulAction.add_card_ofStabilizer_eq
Proof state before:
case e_a.a
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
a : α
⊢ Cardinal.toPartENat 1 = ↑1
Tactic:
exact Iff.mpr Cardinal.toPartENat_eq_natCast_iff rfl
Proof state after:
no goals
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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)
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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))
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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)
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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)
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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⟩
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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)
Theorem: fixingSubgroup_of_insert
Proof 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
Proof state after:
no goals
Theorem: fixingSubgroup_of_insert
Proof 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'⟩
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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'
Proof 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 }
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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)
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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⟩
Proof state after:
no goals
Theorem: fixingSubgroup_of_insert
Proof 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⟩
Proof 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))
Theorem: fixingSubgroup_of_insert
Proof 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 ⊢
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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'
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof state after:
no goals
Theorem: fixingSubgroup_of_insert
Proof 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'
Proof state after:
no goals
Theorem: fixingSubgroup_of_insert
Proof 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
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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⟩
Proof 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
Theorem: fixingSubgroup_of_insert
Proof 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]
Proof state after:
no goals
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
⊢ Function.Bijective ⇑(ofFixingSubgroupEmpty_equivariantMap M α)
Tactic:
constructor
Proof state after:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
⊢ Function.Injective ⇑(ofFixingSubgroupEmpty_equivariantMap M α)

case right
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
⊢ Function.Surjective ⇑(ofFixingSubgroupEmpty_equivariantMap M α)
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case left
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
⊢ Function.Injective ⇑(ofFixingSubgroupEmpty_equivariantMap M α)
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 α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { 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 α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ x = y
Theorem: SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective
Proof state before:
case left.mk.mk
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
x : α
hx : x ∈ ofFixingSubgroup M ∅
y : α
hy : y ∈ ofFixingSubgroup M ∅
hxy :
  (ofFixingSubgroupEmpty_equivariantMap M α) { val := x, property := hx } =
    (ofFixingSubgroupEmpty_equivariantMap M α) { val := y, property := hy }
⊢ x = y
Tactic:
exact hxy
Proof state after:
no goals