awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
have := IsPretransitive.isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
apply :
  Nat.card.{u_2} ↥(ofFixingSubgroup M (s ∩ g • s)) <
    2 *
      Set.ncard.{u_2} (α := ↥(ofFixingSubgroup M (s ∩ g • s)))
        (Set.range (ι := ↥(ofFixingSubgroup M s))
          (⇑(ofFixingSubgroup_of_inclusion M (s := s) (t := s ∩ g • s) ⋯ :
                MulActionHom (M := ↥(fixingSubgroup M s)) (N := ↥(fixingSubgroup M (s ∩ g • s)))
                  (⇑(Subgroup.inclusion ⋯) : (a : ↥(fixingSubgroup M s)) → ↥(fixingSubgroup M (s ∩ g • s)))
                  ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup M (s ∩ g • s))) :
            (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M (s ∩ g • s))))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
apply IsPreprimitive.of_card_lt (f := ofFixingSubgroup_of_inclusion M Set.inter_subset_left)

Premises used: MulAction.IsPreprimitive.of_card_lt
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
rw : (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard
⊢ Nat.card.{u_2} ↥(ofFixingSubgroup M (s ∩ g • s)) <
    2 *
      Set.ncard.{u_2} (α := ↥(ofFixingSubgroup M (s ∩ g • s)))
        (Set.range (ι := ↥(ofFixingSubgroup M s))
          (⇑(ofFixingSubgroup_of_inclusion M (s := s) (t := s ∩ g • s) ⋯ :
                MulActionHom (M := ↥(fixingSubgroup M s)) (N := ↥(fixingSubgroup M (s ∩ g • s)))
                  (⇑(Subgroup.inclusion ⋯) : (a : ↥(fixingSubgroup M s)) → ↥(fixingSubgroup M (s ∩ g • s)))
                  ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup M (s ∩ g • s))) :
            (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup M (s ∩ g • s))))

Tactic:
rw [show Nat.card (ofFixingSubgroup M (s ∩ g • s)) = (s ∩ g • s)ᶜ.ncard from
    Nat.card_coe_set_eq _, Set.ncard_range_of_injective ofFixingSubgroup_of_inclusion_injective,
    show Nat.card (ofFixingSubgroup M s) = sᶜ.ncard from Nat.card_coe_set_eq _, Set.compl_inter]

Premises used: SubMulAction.ofFixingSubgroup_of_inclusion_injective, Set.compl_inter, Nat.card_coe_set_eq, Inter.inter, SetLike.coe, SubMulAction.ofFixingSubgroup, HSMul.hSMul, Set.ncard_range_of_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
⊢ (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard

Tactic:
(Set.ncard_union_lt sᶜ.toFinite (g • s)ᶜ.toFinite ?_).trans_le ?_

Premises used: Compl.compl, Set.ncard_union_lt, Set.toFinite, LT.lt.trans_le, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_1 : ¬Disjoint sᶜ (g • s)ᶜ
refine_2 : sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard
⊢ (sᶜ ∪ (g • s)ᶜ).ncard < 2 * sᶜ.ncard

Tactic:
refine (Set.ncard_union_lt sᶜ.toFinite (g • s)ᶜ.toFinite ?_).trans_le ?_

Premises used: Compl.compl, Set.ncard_union_lt, Set.toFinite, LT.lt.trans_le, HSMul.hSMul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_1 : ¬sᶜ ⊆ g • s
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ¬s ∪ g • s = Set.univ
⊢ ¬Disjoint sᶜ (g • s)ᶜ

Tactic:
rwa [Set.disjoint_compl_right_iff_subset, Set.compl_subset_iff_union]

Premises used: Set.disjoint_compl_right_iff_subset, Set.compl_subset_iff_union
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
hs : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
this : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))
refine_2 : sᶜ.ncard + (g • sᶜ).ncard ≤ 2 * sᶜ.ncard
refine_2₁ : sᶜ.ncard + sᶜ.ncard ≤ 2 * sᶜ.ncard
refine_2₂ refine_2₃ : sᶜ.ncard + sᶜ.ncard ≤ sᶜ.ncard + sᶜ.ncard
⊢ sᶜ.ncard + (g • s)ᶜ.ncard ≤ 2 * sᶜ.ncard

Tactic:
rw [← Set.smul_set_compl, Set.ncard_smul_set, two_mul]

Premises used: two_mul, Set.ncard_smul_set, Set.smul_set_compl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
rw : id '' s
| s

Tactic:
rw [← Set.image_id s]

Premises used: Set.image_id
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
conv_rhs : k • s = id '' s
⊢ k • s = s

Tactic:
conv_rhs => rw [← Set.image_id s]

Premises used: Set.image_id
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
h : ∀ a ∈ s, k • a = id a
⊢ k • s = id '' s

Tactic:
apply Set.image_congr

Premises used: Set.image_congr
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
k : G
hk : Membership.mem (γ := Subgroup G) (fixingSubgroup G s) k
⊢ ∀ a ∈ s, k • a = id a

Tactic:
simpa only [mem_fixingSubgroup_iff, id] using hk

Premises used: id, mem_fixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
rw : x = g⁻¹ • a → x = a
⊢ ¬x = a → ¬g • x = a

Tactic:
rw [not_imp_not, smul_eq_iff_eq_inv_smul]

Premises used: smul_eq_iff_eq_inv_smul, not_imp_not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
a₁ : a = x
⊢ x = a

Tactic:
apply symm

Premises used: symm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
a₁ : g • a = a
⊢ a = x

Tactic:
rw [hgx, ← smul_eq_iff_eq_inv_smul]

Premises used: smul_eq_iff_eq_inv_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
⊢ g • a = a

Tactic:
g.prop

Premises used: Set.Mem, setOf, Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
g : ↥(stabilizer G a)
x : α
hgx : x = g⁻¹ • a
⊢ g • a = a

Tactic:
exact g.prop

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
⊢ carrier (R := ↥(stabilizer G a)) (ofStabilizer G a) = {a}ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a x : α
⊢ Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x ↔ x ≠ a

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton, Not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
b : ↥(ofStabilizer G a)
hb : b ∈ t ∧ (↑b : α) = a
⊢ Membership.mem (γ := Set α) {a} (↑b : α)

Tactic:
simp [hb]
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
b : ↥(ofStabilizer G a)
hb : b ∈ t ∧ (↑b : α) = a
⊢ False

Tactic:
exact b.prop (by simp [hb])

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
x : ↥(ofStabilizer G a)
⊢ (↑x : α) ≠ a

Tactic:
x.prop

Premises used: Set.Mem, setOf, Subtype.prop, Set.singleton, Not
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
rw :
  HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a}ᶜ : Type u_2)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (β := ℕ∞) (1 : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)
      (1 : ℕ∞) =
    (Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk α)

Tactic:
rw [← Cardinal.mk_sum_compl {a}, map_add, add_comm, eq_comm]

Premises used: map_add, Cardinal.mk_sum_compl, eq_comm, add_comm, Singleton.singleton
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
e_a : Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞) (1 : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (β := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a}ᶜ : Type u_2)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (β := ℕ∞) (1 : ℕ∞)
      ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk ↥(ofStabilizer G a)) : ℕ∞)

Tactic:
congr
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
⊢ Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (↑{a} : Type u_2)) : ℕ∞) (1 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
rw :
  ∀ (x : α),
    Membership.mem (γ := Finset α) {a}ᶜ x ↔
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
⊢ Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α

Tactic:
rw [Nat.subtype_card {a}ᶜ, ← Finset.card_singleton a, Finset.card_compl_add_card,
    Nat.card_eq_fintype_card]

Premises used: Finset.card_compl_add_card, Compl.compl, Nat.subtype_card, Singleton.singleton, Nat.card_eq_fintype_card, Finset.card_singleton
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
this : Fintype α := Fintype.ofFinite α
⊢ ∀ (x : α),
    Membership.mem (γ := Finset α) {a}ᶜ x ↔
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x

Tactic:
simp [mem_ofStabilizer_iff]

Premises used: SubMulAction.mem_ofStabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
let let₁ let₂ : Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α
let₃ :
  let this := Fintype.ofFinite α;
  ∀ (x : α),
    Membership.mem (γ := Finset α) {a}ᶜ x ↔
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x
⊢ Nat.card.{u_2} ↥(ofStabilizer G a) + 1 = Nat.card α

Tactic:
classical
  let := Fintype.ofFinite α
  rw [Nat.subtype_card {a}ᶜ, ← Finset.card_singleton a, Finset.card_compl_add_card,
    Nat.card_eq_fintype_card]
  simp [mem_ofStabilizer_iff]

Premises used: Finset.card_compl_add_card, SubMulAction.mem_ofStabilizer_iff, Nat.card_eq_fintype_card, Finset.card_singleton
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
a : α
⊢ Nat.card.{u_2} ↥(ofStabilizer G a) = Nat.card α - 1

Tactic:
Nat.eq_sub_of_add_eq (nat_card_ofStabilizer_add_one_eq G a)

Premises used: SubMulAction.nat_card_ofStabilizer_add_one_eq, Nat.eq_sub_of_add_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G_1 : Type u_1
inst : Group G_1
α_1 : Type u_2
inst_1 : MulAction G_1 α_1
G : Type u_3
inst_2 : AddGroup G
α : Type u_4
inst_3 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x : ↥(SubAddAction.ofStabilizer G a)
hy : Membership.mem (γ := Set α) {b} (g +ᵥ (↑x : α))
⊢ Membership.mem (γ := Set α) {a} (↑x : α)

Tactic:
simpa [hg] using hy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G_1 : Type u_1
inst : Group G_1
α_1 : Type u_2
inst_1 : MulAction G_1 α_1
G : Type u_3
inst_2 : AddGroup G
α : Type u_4
inst_3 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
x_1 : ↥(AddAction.stabilizer G a)
x : ↥(SubAddAction.ofStabilizer G a)
k : G
hk : Membership.mem (γ := AddSubgroup G) (AddAction.stabilizer G a) k
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubAddAction.{u_3, u_4} (↥(AddAction.stabilizer G b)) α) (SubAddAction.ofStabilizer G b) x)
      (g +ᵥ
        (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := AddSubgroup G) (AddAction.stabilizer G a) x) k hk +ᵥ x) :
          α))
      ⋯ =
    HVAdd.hVAdd (α := ↥(AddAction.stabilizer G b)) (β := ↥(SubAddAction.ofStabilizer G b))
      ((AddAction.stabilizerEquivStabilizer hg : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b))
          (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := AddSubgroup G) (AddAction.stabilizer G a) x) k hk) :
        ↥(AddAction.stabilizer G b))
      (Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubAddAction.{u_3, u_4} (↥(AddAction.stabilizer G b)) α) (SubAddAction.ofStabilizer G b) x)
        (g +ᵥ (↑x : α)) ⋯)

Tactic:
simp [← SetLike.coe_eq_coe, AddAction.addSubgroup_vadd_def,
      AddAction.stabilizerEquivStabilizer_apply, ← vadd_assoc]

Premises used: vadd_assoc, SetLike.coe_eq_coe, AddAction.addSubgroup_vadd_def, AddAction.stabilizerEquivStabilizer_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
hy : Membership.mem (γ := Set α) {b} (g • (↑x : α))
⊢ Membership.mem (γ := Set α) {a} (↑x : α)

Tactic:
simpa [hg] using hy
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(stabilizer G a)
k : G
hk : Membership.mem (γ := Subgroup G) (stabilizer G a) k
⊢ ∀ (x : ↥(ofStabilizer G a)),
    Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G b)) α) (ofStabilizer G b) x)
        (g • (↑(Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) k hk • x) : α)) ⋯ =
      HSMul.hSMul (α := ↥(stabilizer G b)) (β := ↥(ofStabilizer G b))
        ((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b))
            (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (stabilizer G a) x) k hk) :
          ↥(stabilizer G b))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G b)) α) (ofStabilizer G b) x) (g • (↑x : α)) ⋯)

Tactic:
simp [← SetLike.coe_eq_coe, subgroup_smul_def, stabilizerEquivStabilizer, ← smul_assoc]

Premises used: MulAction.stabilizerEquivStabilizer, smul_assoc, SetLike.coe_eq_coe, MulAction.subgroup_smul_def
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
⊢ (↑((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b)) x) : α) = g • (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_3
inst : AddGroup G
α : Type u_4
inst_1 : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
h₁ :
  ∀ (x : ↥(AddAction.stabilizer G a)),
    Eq (α := G)
      (↑(Function.comp (β := ↥(AddAction.stabilizer G b))
            (⇑(AddAction.stabilizerEquivStabilizer hh) :
              (a : ↥(AddAction.stabilizer G b)) → ↥(AddAction.stabilizer G c))
            (⇑(AddAction.stabilizerEquivStabilizer hg) :
              (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b))
            x) :
        G)
      (↑((AddAction.stabilizerEquivStabilizer hk : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G c)) x) :
        G)
⊢ Eq (α := ↥(AddAction.stabilizer G a) → ↥(AddAction.stabilizer G c))
    (Function.comp (β := ↥(AddAction.stabilizer G b))
      (⇑(AddAction.stabilizerEquivStabilizer hh) : (a : ↥(AddAction.stabilizer G b)) → ↥(AddAction.stabilizer G c))
      (⇑(AddAction.stabilizerEquivStabilizer hg) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b)))
    (⇑(AddAction.stabilizerEquivStabilizer hk) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G c))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_3
inst : AddGroup G
α : Type u_4
inst_1 : AddAction G α
g h k : G
a b c : α
hg : b = g +ᵥ a
hh : c = h +ᵥ b
hk : c = k +ᵥ a
H : k = h + g
x : ↥(AddAction.stabilizer G a)
⊢ Eq (α := G)
    (↑(Function.comp (β := ↥(AddAction.stabilizer G b))
          (⇑(AddAction.stabilizerEquivStabilizer hh) : (a : ↥(AddAction.stabilizer G b)) → ↥(AddAction.stabilizer G c))
          (⇑(AddAction.stabilizerEquivStabilizer hg) : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G b))
          x) :
      G)
    (↑((AddAction.stabilizerEquivStabilizer hk : (a : ↥(AddAction.stabilizer G a)) → ↥(AddAction.stabilizer G c)) x) :
      G)

Tactic:
simp [AddAction.stabilizerEquivStabilizer, H, AddAut.conj, ← add_assoc]

Premises used: add_assoc, AddAction.stabilizerEquivStabilizer, AddAut.conj
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
h₁ :
  ∀ (x : ↥(stabilizer G a)),
    Eq (α := G)
      (↑(Function.comp (β := ↥(stabilizer G b))
            (⇑(stabilizerEquivStabilizer hh) : (a : ↥(stabilizer G b)) → ↥(stabilizer G c))
            (⇑(stabilizerEquivStabilizer hg) : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) :
        G)
      (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
⊢ Eq (α := ↥(stabilizer G a) → ↥(stabilizer G c))
    (Function.comp (β := ↥(stabilizer G b))
      (⇑(stabilizerEquivStabilizer hh) : (a : ↥(stabilizer G b)) → ↥(stabilizer G c))
      (⇑(stabilizerEquivStabilizer hg) : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)))
    (⇑(stabilizerEquivStabilizer hk) : (a : ↥(stabilizer G a)) → ↥(stabilizer G c))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(stabilizer G a)
⊢ Eq (α := G)
    (↑(Function.comp (β := ↥(stabilizer G b))
          (⇑(stabilizerEquivStabilizer hh) : (a : ↥(stabilizer G b)) → ↥(stabilizer G c))
          (⇑(stabilizerEquivStabilizer hg) : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)

Tactic:
simp [stabilizerEquivStabilizer, H, MulAut.conj, ← mul_assoc]

Premises used: MulAction.stabilizerEquivStabilizer, mul_assoc, MulAut.conj
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(ofStabilizer G a)
⊢ Eq (α := ↥(ofStabilizer G c))
    ((conjMap hh : (a : ↥(ofStabilizer G b)) → ↥(ofStabilizer G c))
        ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b)) x) :
      ↥(ofStabilizer G c))
    ((conjMap hk : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x : ↥(ofStabilizer G c))

Tactic:
simp [← Subtype.coe_inj, conjMap_apply, H, mul_smul]

Premises used: Subtype.coe_inj, SubMulAction.ofStabilizer.conjMap_apply, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G a)
⊢ (conjMap ⋯ : (a_1 : ↥(ofStabilizer G b)) → ↥(ofStabilizer G a))
      ((conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b)) x) =
    x

Tactic:
simp [← Subtype.coe_inj, conjMap_apply]

Premises used: Subtype.coe_inj, SubMulAction.ofStabilizer.conjMap_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
x : ↥(ofStabilizer G b)
⊢ (conjMap hg : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G b))
      ((conjMap ⋯ : (a_1 : ↥(ofStabilizer G b)) → ↥(ofStabilizer G a)) x) =
    x

Tactic:
simp [← Subtype.coe_inj, conjMap_apply]

Premises used: Subtype.coe_inj, SubMulAction.ofStabilizer.conjMap_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
a₁ :
  ∀ (x : ↥(ofStabilizer G a)),
    Eq.{u_2 + 1} (α := α) (↑(((conjMap hh).comp (conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)
      (↑((conjMap hk : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)
⊢ (conjMap hh).comp (conjMap hg) = conjMap hk

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
g h k : G
a b c : α
hg : b = g • a
hh : c = h • b
hk : c = k • a
H : k = h * g
x : ↥(ofStabilizer G a)
⊢ Eq.{u_2 + 1} (α := α) (↑(((conjMap hh).comp (conjMap hg) : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)
    (↑((conjMap hk : (a : ↥(ofStabilizer G a)) → ↥(ofStabilizer G c)) x) : α)

Tactic:
simpa using conjMap_comp_apply H x

Premises used: SubMulAction.ofStabilizer.conjMap_comp_apply