-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.WeylGroup (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
B : P.InvariantForm
g g₁ g₂ : P.Aut
hg₁ : g₁ ∈ P.weylGroup
hg₂ : g₂ ∈ P.weylGroup
hg₁' :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • x) : M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₁ hg₁ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
hg₂' :
  ∀ (x y : M),
    Eq.{u_2 + 1} (α := R)
      ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • x) : M →ₗ[R] R) :
            (a : M) → R)
          (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) g₂ hg₂ • y) :
        R)
      ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
x y : M
mul :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
                  Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
                x) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
            Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
          y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
mul₁ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
                Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ *
            Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂) •
          y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
mul₂ :
  Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R)
              (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
                Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₁ hg₁ •
          Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) ⋯ • x) :
            M →ₗ[R] R) :
          (a : M) → R)
        (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup) (g₁ * g₂) ⋯ • y) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have mul₃ : Eq.{u_2 + 1} (α := R)
  ((((B.form : (a : M) → M →ₗ[R] R) (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • x) :
          M →ₗ[R] R) :
        (a : M) → R)
      (Subtype.mk (p := fun (x : P.Aut) ↦ x ∈ P.weylGroup.toSubmonoid) g₂ hg₂ • y) :
    R)
  ((((B.form : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: rw [← Submonoid.mk_mul_mk _ _ _ hg₁ hg₂, mul_smul, mul_smul, hg₁', hg₂']