awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g • a
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯
have h : ∀ (x : ↥(stabilizer G b)),
  Eq.{u_1 + 1} (α := G) (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
    (↑((stabilizerEquivStabilizer sorry : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
g : G
a b : α
hg : b = g⁻¹ • a
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm
have h : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
    (↑(((stabilizerEquivStabilizer sorry).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
⊢ Eq (α := AddSubgroup G) (stabilizer G (g +ᵥ a))
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
have h : ∀ (h : G),
  Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
Tactic: ext h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₁ : h +ᵥ g +ᵥ a = g +ᵥ a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₂ : -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₃ : (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₃ :
  (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₄ : (-g + h + g) +ᵥ a = -g +ᵥ g +ᵥ a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₃ :
  (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₄ :
  (-g + h + g) +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₅ : (-g + h + g) +ᵥ a = (-g + g) +ᵥ a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₃ :
  (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₄ :
  (-g + h + g) +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₅ :
  (-g + h + g) +ᵥ a = (-g + g) +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₆ : (-g + h + g) +ᵥ a = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₃ :
  (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₄ :
  (-g + h + g) +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₅ :
  (-g + h + g) +ᵥ a = (-g + g) +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₆ :
  (-g + h + g) +ᵥ a = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₇ : (-g + h + g) +ᵥ a = a ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a : α
h : G
h₁ :
  h +ᵥ g +ᵥ a = g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₂ :
  -g +ᵥ h +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₃ :
  (-g + h) +ᵥ g +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₄ :
  (-g + h + g) +ᵥ a = -g +ᵥ g +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₅ :
  (-g + h + g) +ᵥ a = (-g + g) +ᵥ a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₆ :
  (-g + h + g) +ᵥ a = HVAdd.hVAdd.{u_1, u_2, u_2} (α := G) 0 a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
h₇ :
  (-g + h + g) +ᵥ a = a ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
⊢ Membership.mem (γ := AddSubgroup G) (stabilizer G (g +ᵥ a)) h ↔
    Membership.mem (γ := AddSubgroup G)
      (AddSubgroup.map
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (stabilizer G a))
      h
have h₈ : Membership.mem (γ := AddSubgroup G) (stabilizer G a) (-g + h + g) ↔
  Membership.mem (γ := AddSubgroup G)
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
    h
Tactic: rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
    neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
    AddAut.conj_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g_1 h_1 k_1 : G
a_1 b_1 c_1 : α
g h k : G
a b c : α
hg : b = g +ᵥ a
⊢ Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G b)
have rw : Eq (α := AddSubgroup G)
  (AddSubgroup.map
    (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
          AddAut G) :
      G →+ G)
    (stabilizer G a))
  (stabilizer G (g +ᵥ a))
Tactic: rw [hg, stabilizer_vadd_eq_stabilizer_map_conj g a, ← AddEquiv.toAddMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g_1 h_1 k_1 : G
a_1 b_1 c_1 : α
g h k : G
a b c : α
hg : b = g +ᵥ a
rw :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G (g +ᵥ a))
⊢ Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G b)
have rw₁ : Eq (α := AddSubgroup G)
  (AddSubgroup.map
    (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
          AddAut G) :
      G →+ G)
    (stabilizer G a))
  (AddSubgroup.map
    (AddEquiv.toAddMonoidHom
      ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
    (stabilizer G a))
Tactic: rw [hg, stabilizer_vadd_eq_stabilizer_map_conj g a, ← AddEquiv.toAddMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g_1 h_1 k_1 : G
a_1 b_1 c_1 : α
g h k : G
a b c : α
hg : b = g +ᵥ a
rw :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G (g +ᵥ a))
rw₁ :
  Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (AddSubgroup.map
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (stabilizer G a))
⊢ Eq (α := AddSubgroup G)
    (AddSubgroup.map
      (↑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        G →+ G)
      (stabilizer G a))
    (stabilizer G b)
have rw₂ : Eq (α := AddSubgroup G)
  (AddSubgroup.map
    (AddEquiv.toAddMonoidHom
      ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
    (stabilizer G a))
  (AddSubgroup.map
    (AddEquiv.toAddMonoidHom
      ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
    (stabilizer G a))
Tactic: rw [hg, stabilizer_vadd_eq_stabilizer_map_conj g a, ← AddEquiv.toAddMonoidHom_eq_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
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
⊢ (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk
have h₁ : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G)
    (↑(((stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) :
            (a : ↥(stabilizer G a)) → ↥(stabilizer G c))
          x) :
      G)
    (↑((stabilizerEquivStabilizer hk : (a : ↥(stabilizer G a)) → ↥(stabilizer G c)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
a : α
⊢ Eq (α := ↥(stabilizer G a) ≃+ ↥(stabilizer G a)) (stabilizerEquivStabilizer ⋯) (AddEquiv.refl ↥(stabilizer G a))
have h : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer sorry : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
    (↑((AddEquiv.refl ↥(stabilizer G a) : (a_1 : ↥(stabilizer G a)) → ↥(stabilizer G a)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = g +ᵥ a
⊢ (stabilizerEquivStabilizer hg).symm = stabilizerEquivStabilizer ⋯
have h : ∀ (x : ↥(stabilizer G b)),
  Eq.{u_1 + 1} (α := G) (↑(((stabilizerEquivStabilizer hg).symm : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
    (↑((stabilizerEquivStabilizer sorry : (a_1 : ↥(stabilizer G b)) → ↥(stabilizer G a)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : AddGroup G
inst_1 : AddAction G α
g : G
a b : α
hg : b = -g +ᵥ a
⊢ stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer ⋯).symm
have h : ∀ (x : ↥(stabilizer G a)),
  Eq.{u_1 + 1} (α := G) (↑((stabilizerEquivStabilizer hg : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
    (↑(((stabilizerEquivStabilizer sorry).symm : (a : ↥(stabilizer G a)) → ↥(stabilizer G b)) x) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
⊢ Membership.mem (γ := Subgroup (Perm α)) (MulAction.stabilizer (Perm α) S) (swap a b) ↔ (a ∈ S ↔ b ∈ S)
have rw : (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
Tactic: rw [MulAction.mem_stabilizer_iff, Set.ext_iff, ← swap_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
⊢ (∀ (x : α), x ∈ (swap a b)⁻¹ • S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
have simp_rw : (∀ (x : α), (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S) ↔ (a ∈ S ↔ b ∈ S)
Tactic: simp_rw [Set.mem_inv_smul_set_iff, Perm.smul_def, swap_apply_def]