-- Lean 4 proof step from Mathlib.Algebra.Algebra.Subalgebra.Pointwise (goal)
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S T : Subalgebra R A
x_1 : A
hx_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x_1
x y : A
h : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) x
h_1 : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ((↑S : Set A) ∪ (↑T : Set A))) y
hx :
  x ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
hy :
  y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
this :
  x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A) *
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
refine_3 :
  ∀
    (this :
      x * y ∈
        HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
          (HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
            (HMul.hMul (α := Submodule R A) (β := Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
              ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)))),
    x * y ∈
      HMul.hMul (α := Submodule R A) (β := Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
⊢ x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
have refine_3₁ : ∀
  (this :
    x * y ∈
      HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
        (HMul.hMul (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
          (HMul.hMul (α := Submodule R A) (β := Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
            ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)))),
  x * y ∈
    HMul.hMul (α := Submodule R A) (β := Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      ((toSubmodule : (a : Subalgebra R A) → Submodule R A) T : Submodule R A)
Tactic: rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S),
    isIdempotentElem_toSubmodule, mul_comm T.toSubmodule, ← mul_assoc,
    isIdempotentElem_toSubmodule] at this
Cleared hypotheses: this