awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : α ⧸ H
g₁ g₂ : α
h : g₁⁻¹ * g₂ ∈ H
rw : g₁⁻¹ • x ∈ orbit.{u, v} (↥H) (g₂⁻¹ • x)
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]

Premises used: Quotient.eq'', MulAction.orbitRel_apply, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : α ⧸ H
g₁ g₂ : α
h : g₁⁻¹ * g₂ ∈ H
⊢ (fun (m : ↥H) ↦ m • g₂⁻¹ • x) (Subtype.mk (p := fun (x : α) ↦ x ∈ H) (g₁⁻¹ * g₂) h) = g₁⁻¹ • x

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
q : α ⧸ H
g₁ g₂ : α
h : g₁⁻¹ * g₂ ∈ H
⊢ g₁⁻¹ • x ∈ orbit.{u, v} (↥H) (g₂⁻¹ • x)

Tactic:
exact ⟨⟨_, h⟩, by simp [mul_smul]⟩
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
y : orbitRel.Quotient.{u, v} (↥H) β
h :
  ∀ (a : β),
    Eq (α := orbitRel.Quotient.{u, v} (↥H) β)
      ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β))
        ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
            Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
          (Quotient.mk'' a)))
      (Quotient.mk'' a)
⊢ (fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β))
      ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
          Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
        y) =
    y

Tactic:
cases y using Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
h : (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x ∈ orbit.{u, v} (↥H) a
⊢ ⟦(Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x⟧ = Quotient.mk'' a

Tactic:
rw [← @Quotient.mk''_eq_mk, Quotient.eq'', orbitRel_apply]

Premises used: Quotient.eq'', MulAction.orbitRel_apply, Quotient.mk''_eq_mk
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
⊢ a ∈ orbit.{u, v} (↥H) a

Tactic:
mem_orbit_self _

Premises used: MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
h : (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x = a
⊢ (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x ∈ orbit.{u, v} (↥H) a

Tactic:
convert! mem_orbit_self _

Premises used: MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
a : β
h : x = Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯ • a
h₁ h₂ : x = x
⊢ (Exists.choose (p := fun (m : α) ↦ m • a = x) ⋯)⁻¹ • x = a

Tactic:
rw [inv_smul_eq_iff, (exists_smul_eq α _ x).choose_spec]

Premises used: Exists.choose_spec, inv_smul_eq_iff, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α ⧸ H
h :
  ∀ (g : α),
    Eq (α := α ⧸ H)
      ((fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
          Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
        ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β))
          (Quotient.mk'' g)))
      (Quotient.mk'' g)
⊢ (fun (q : orbitRel.Quotient.{u, v} (↥H) β) ↦
        Quotient.liftOn' q (fun (y : β) ↦ (↑(Exists.choose (p := fun (m : α) ↦ m • y = x) ⋯) : α ⧸ H)) ⋯)
      ((fun (q : α ⧸ H) ↦ (Quotient.liftOn' q (fun (g : α) ↦ ⟦g⁻¹ • x⟧) ⋯ : orbitRel.Quotient.{u, v} (↥H) β)) g) =
    g

Tactic:
cases g using Quotient.inductionOn' with | _ g
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g ∈ H
⊢ Eq (α := α ⧸ H) (Quotient.mk'' (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)) (Quotient.mk'' g)

Tactic:
rw [Quotient.eq'', leftRel_eq]

Premises used: QuotientGroup.leftRel_eq, Quotient.eq''
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
⊢ 1 ∈ H

Tactic:
one_mem H

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g ∈ H

Tactic:
convert! one_mem H

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : MulAction α β
x : β
inst_2 : IsPretransitive α β
inst_3 : IsCancelSMul α β
H : Subgroup α
g : α
h : Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = g
h₁ : g = Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯
h₂ : g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ = 1
h₃ : Membership.mem (γ := Subgroup α) ⊥ (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₄ :
  Membership.mem (γ := Subgroup α) (stabilizer α (g⁻¹ • x)) (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)
h₅ : (g⁻¹ * Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯) • g⁻¹ • x = g⁻¹ • x
h₆ : g⁻¹ • Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯ • g⁻¹ • x = g⁻¹ • x
h₇ h₈ : g⁻¹ • x = g⁻¹ • x
⊢ (Exists.choose (p := fun (m : α) ↦ m • g⁻¹ • x = x) ⋯)⁻¹ * g = 1

Tactic:
rw [inv_mul_eq_one, eq_comm, ← inv_mul_eq_one, ← Subgroup.mem_bot,
        ← IsCancelSMul.stabilizer_eq_bot (g⁻¹ • x), mem_stabilizer_iff, mul_smul,
        (exists_smul_eq α (g⁻¹ • x) x).choose_spec]

Premises used: Exists.choose_spec, eq_comm, Inv.inv, HSMul.hSMul, MulAction.mem_stabilizer_iff, MulAction.exists_smul_eq, SemigroupAction.mul_smul, Subgroup.mem_bot, IsCancelSMul.stabilizer_eq_bot, inv_mul_eq_one
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]

Premises used: Fintype.card_congr, ConjAct.toConjAct, MulEquiv.toEquiv
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
H : 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]

Premises used: Nat.mul_div_cancel, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, ConjAct
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)

Tactic:
simp_rw [ConjAct.orbit_eq_carrier_conjClasses]

Premises used: ConjAct.orbit_eq_carrier_conjClasses
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
Fintype.card_pos_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
exact Fintype.card_pos_iff.mpr inferInstance

Premises used: Iff.mpr, inferInstance, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : Fintype G
g : G
inst_2 : Fintype (↑(carrier (ConjClasses.mk g)) : Type u_1)
inst_3 : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
rw rw₁ rw₂ :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (ConjAct G) / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
rw₃ :
  Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card.{u_1} (↑(MulAction.orbit (ConjAct G) g) : Type u_1)
H H₁ : 0 < Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card.{u_1} (↑(carrier (ConjClasses.mk g)) : Type u_1) =
    Fintype.card G / Fintype.card.{u_1} ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
classical
  rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv]
  rw [← MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel]
  · simp_rw [ConjAct.orbit_eq_carrier_conjClasses]
  · exact Fintype.card_pos_iff.mpr inferInstance

Premises used: Fintype.card_congr, Iff.mpr, Nat.mul_div_cancel, inferInstance, ConjAct.toConjAct, MulEquiv.toEquiv, ConjAct.orbit_eq_carrier_conjClasses, Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : H.normalCore ≤ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))
a₁ : MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)) ≤ H.normalCore
⊢ H.normalCore = MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
a :
  ∀ (x : G ⧸ H),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          x :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) x : G ⧸ H)
⊢ Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g

Tactic:
apply Equiv.Perm.ext

Premises used: Equiv.Perm.ext
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          x :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) x : G ⧸ H)

Tactic:
fun q ↦ QuotientGroup.induction_on q ?_

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
a :
  ∀ (q : G ⧸ H) (z : G),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          (↑z : G ⧸ H) :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) (↑z : G ⧸ H) : G ⧸ H)
⊢ ∀ (x : G ⧸ H),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          x :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) x : G ⧸ H)

Tactic:
refine fun q ↦ QuotientGroup.induction_on q ?_
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          (↑z : G ⧸ H) :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) (↑z : G ⧸ H) : G ⧸ H)

Tactic:
fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)

Premises used: Iff.mpr, MulAction.Quotient.smul_mk, QuotientGroup.eq, Quot.map, Quotient.map', Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
a : ∀ (g' : G), (g • g')⁻¹ * g' ∈ H
⊢ ∀ (z : G),
    Eq (α := G ⧸ H)
      ((((MulAction.toPermHom G (G ⧸ H) : (a : G) → Equiv.Perm (G ⧸ H)) g : Equiv.Perm (G ⧸ H)) : (a : G ⧸ H) → G ⧸ H)
          (↑z : G ⧸ H) :
        G ⧸ H)
      ((1 : (a : G ⧸ H) → G ⧸ H) (↑z : G ⧸ H) : G ⧸ H)

Tactic:
refine fun g' => (MulAction.Quotient.smul_mk H g g').trans (QuotientGroup.eq.mpr ?_)

Premises used: Iff.mpr, MulAction.Quotient.smul_mk, QuotientGroup.eq, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
a : g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
⊢ (g • g')⁻¹ * g' ∈ H

Tactic:
rw [smul_eq_mul, mul_inv_rev, ← inv_inv g', inv_inv]

Premises used: inv_inv, mul_inv_rev, smul_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Tactic:
H.normalCore.inv_mem hg g'⁻¹

Premises used: Set.Mem, Inv.inv, Subgroup.inv_mem, Subgroup.normalCore
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Tactic:
exact H.normalCore.inv_mem hg g'⁻¹

Premises used: Inv.inv, Subgroup.inv_mem, Subgroup.normalCore
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)) ≤ H.normalCore

Tactic:
(Subgroup.normal_le_normalCore.mpr fun g hg => ?_)

Premises used: Iff.mpr, Subgroup.normal_le_normalCore
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a :
  ∀ (g : G)
    (hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g),
    g ∈ H
⊢ MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H)) ≤ H.normalCore

Tactic:
refine (Subgroup.normal_le_normalCore.mpr fun g hg => ?_)

Premises used: Iff.mpr, Subgroup.normal_le_normalCore
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g
a : Eq (α := G ⧸ H) (↑(g * 1) : G ⧸ H) (↑1 : G ⧸ H)
⊢ g ∈ H

Tactic:
rw [← H.inv_mem_iff, ← mul_one g⁻¹, ← QuotientGroup.eq, ← mul_one g]

Premises used: QuotientGroup.eq, Inv.inv, Subgroup.inv_mem_iff, mul_one
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g
⊢ Eq (α := G ⧸ H) (↑(g * 1) : G ⧸ H) (↑1 : G ⧸ H)

Tactic:
(MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

Premises used: QuotientGroup.mk, MulAction.Quotient.smul_mk, Equiv.Perm.ext_iff, Iff.mp, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (MonoidHom.ker (M := Equiv.Perm (G ⧸ H)) (MulAction.toPermHom G (G ⧸ H))) g
⊢ Eq (α := G ⧸ H) (↑(g * 1) : G ⧸ H) (↑1 : G ⧸ H)

Tactic:
exact (MulAction.Quotient.smul_mk H g 1).symm.trans (Equiv.Perm.ext_iff.mp hg (1 : G))

Premises used: QuotientGroup.mk, MulAction.Quotient.smul_mk, Equiv.Perm.ext_iff, Iff.mp, OfNat.ofNat, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
g x : G
⊢ Eq (α := (↑(commutatorSet G) : Type u_1))
    ((quotientCentralizerEmbedding g : (a : G ⧸ centralizer {g}) → (↑(commutatorSet G) : Type u_1))
        (↑x : G ⧸ centralizer {g}) :
      (↑(commutatorSet G) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ commutatorSet G) ⁅x, g⁆ ⋯ : { x : G // x ∈ commutatorSet G })

Tactic:
rfl

Premises used: Quotient.liftOn', MulAction.ofQuotientStabilizer, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Quotient
Goal:
G : Type u_1
inst : Group G
S : Set G
hS : Eq (α := Subgroup G) (closure S) ⊤
g : G
s : (↑S : Type u_1)
⊢ Eq (α := (↑(commutatorSet G) : Type u_1))
    ((quotientCenterEmbedding (S := S) hS : (a : G ⧸ center G) → (↑S : Type u_1) → (↑(commutatorSet G) : Type u_1))
        (↑g : G ⧸ center G) s :
      (↑(commutatorSet G) : Type u_1))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ commutatorSet G) ⁅g, (↑s : G)⁆ ⋯ : { x : G // x ∈ commutatorSet G })

Tactic:
rfl

Premises used: Quotient.liftOn', MulAction.ofQuotientStabilizer, rfl
-- Module: Mathlib.GroupTheory.GroupAction.Ring
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
⊢ HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.Ring
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
x y : R
n : ℕ
ih : (n • x) • y = n • x • y
succ : (n • x + x) • y = n • x • y + x • y
succ₁ : (n • x + x) • y = (n • x) • y + x • y
succ₂ : (n • x + x) * y = n • x * y + x * y
⊢ ((n + 1) • x) • y = (n + 1) • x • y

Tactic:
simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]

Premises used: add_mul, smul_eq_mul, succ_nsmul
-- Module: Mathlib.GroupTheory.GroupAction.Ring
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
n : ℕ
x y : R
zero : HSMul.hSMul (α := ℕ) 0 x • y = HSMul.hSMul (α := ℕ) 0 (x • y)
succ : ∀ (n : ℕ) (ih : (n • x) • y = n • x • y), ((n + 1) • x) • y = (n + 1) • x • y
⊢ (n • x) • y = n • x • y

Tactic:
induction n with
    | zero => simp
    | succ n ih => simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul]

Premises used: add_mul, smul_eq_mul, succ_nsmul
-- Module: Mathlib.GroupTheory.GroupAction.Ring
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
simp_rw : (n • x) • y = n • x • y
⊢ HSMul.hSMul (α := ℤ) (↑n : ℤ) x • y = HSMul.hSMul (α := ℤ) (↑n : ℤ) (x • y)

Tactic:
simp_rw [natCast_zsmul, smul_assoc]

Premises used: smul_assoc, natCast_zsmul
-- Module: Mathlib.GroupTheory.GroupAction.Ring
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
n_1 : ℤ
x y : R
n : ℕ
simp_rw : -((n + 1) • x) • y = -((n + 1) • x • y)
simp_rw₁ : -((n + 1) • x) * y = -((n + 1) • (x * y))
simp_rw₂ : -((n + 1) • x * y) = -((n + 1) • (x * y))
⊢ (-[n+1] • x) • y = -[n+1] • x • y

Tactic:
simp_rw [negSucc_zsmul, smul_eq_mul, neg_mul, smul_mul_assoc]

Premises used: smul_mul_assoc, negSucc_zsmul, neg_mul, smul_eq_mul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
s : Set M
x : M
⊢ Membership.mem (γ := SubMulAction R M) (closure R s) x ↔ ∀ (p : SubMulAction R M), s ⊆ (↑p : Set M) → x ∈ p

Tactic:
Set.mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
s : Set M
⊢ s ⊆ (↑(closure R s) : Set M)

Tactic:
fun _ h => mem_closure.2 fun _ hp => hp h

Premises used: Iff.mpr, SubMulAction.mem_closure, Set.Subset
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
s : Set M
x : M
hx : x ∈ s
⊢ Membership.mem (γ := SubMulAction R M) (closure R s) x

Tactic:
subset_closure hx

Premises used: SubMulAction.subset_closure
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
s : Set M
p : SubMulAction R M
⊢ closure R s ≤ p ↔ s ⊆ (↑p : Set M)

Tactic:
⟨subset_closure.trans, fun ss _ h => mem_closure.1 h _ ss⟩

Premises used: HasSubset.Subset.trans, SubMulAction.mem_closure, SubMulAction.subset_closure, Iff.intro, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
s t : Set M
h : s ⊆ t
⊢ LE.le (α := SubMulAction R M) (closure R s) (closure R t)

Tactic:
closure_le.2 <| h.trans subset_closure

Premises used: Iff.mpr, SubMulAction.closure_le, HasSubset.Subset.trans, SubMulAction.subset_closure
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
Goal:
R : Type u_1
M : Type u_2
inst : SMul R M
p : SubMulAction R M
⊢ p.FG ↔ ∃ (s : Finset M), p = closure R (↑s : Set M)

Tactic:
Set.exists_finite_iff_finset

Premises used: SubMulAction.FG, Set.exists_finite_iff_finset
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
n : ℕ
g : G
s : (↑(powersetCard α n) : Type u_2)
⊢ (↑(g • s) : Finset α) = g • (↑s : Finset α)

Tactic:
SubMulAction.val_smul (p := subMulAction G α n) g s

Premises used: SubMulAction.val_smul
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
n : ℕ
s : (↑(powersetCard α n) : Type u_2)
h :
  ∀ (g : G),
    Membership.mem (γ := Subgroup G) (stabilizer G s) g ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) g
⊢ Eq (α := Subgroup G) (stabilizer G s) (stabilizer G (↑s : Set α))

Tactic:
ext g
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
n : ℕ
s : (↑(powersetCard α n) : Type u_2)
g : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G s) g ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑s : Set α)) g

Tactic:
simp [mem_stabilizer_iff, ← Subtype.coe_inj, ← coe_inj]

Premises used: Subtype.coe_inj, Finset.coe_inj, MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1 ↔
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro