-- Module: Mathlib.GroupTheory.GroupAction.Basic
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
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
h₉ :
  Membership.mem (γ := AddSubgroup G) (stabilizer G a) (-g + h + g) ↔
    Membership.mem (α := G) (γ := AddSubgroup G) (stabilizer G a)
      ((AddEquiv.symm
              ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                ((AddAut.conj : (a : G) → Additive (AddAut G)) g)) :
            (a : G) → G)
          h :
        G)
h₁₀ h₁₁ :
  Membership.mem (γ := AddSubgroup G) (stabilizer G a) (-g + h + g) ↔
    Membership.mem (γ := AddSubgroup G) (stabilizer G a) (-g + 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:
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]

Premises used: vadd_vadd, AddAction.mem_stabilizer_iff, AddAut.conj_symm_apply, zero_vadd, neg_add_cancel, AddSubgroup.mem_map_equiv, vadd_left_cancel_iff, Neg.neg