-- 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
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
⊢ 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 (α := 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)
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]