-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
F : Type u_1
E : Type u_2
inst : CommSemiring F
inst_1 : Semiring E
inst_2 : Algebra F E
b : F →ₗ[F] E
hb : Surjective.{u_1 + 1, u_2 + 1} (α := F) (β := E) (⇑b : (a : F) → E)
x y z : F
hz : Eq.{u_2 + 1} (α := E) ((b : (a : F) → E) z : E) (1 : E)
hy :
  x • HSMul.hSMul (β := E) z ((b : (a : F) → E) y : E) =
    x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)
rwa :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z • y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₁ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (z * y) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₂ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • z • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) 1 : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₃ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (β := E) (HSMul.hSMul (β := E) z ((b : (a : F) → E) 1 : E)) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₄ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (HSMul.hSMul (β := F) z 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₅ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) (z * 1) : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₆ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y * z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₇ :
  ∀
    (hy :
      HSMul.hSMul (β := E) x ((b : (a : F) → E) (y • z) : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
rwa₈ :
  ∀
    (hy :
      x • HSMul.hSMul (β := E) y ((b : (a : F) → E) z : E) =
        x • HMul.hMul (α := E) (β := E) ((b : (a : F) → E) z : E) ((b : (a : F) → E) 1 : E)),
    Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
have rwa₉ : ∀ (hy : x • HSMul.hSMul (β := E) y 1 = x • HMul.hMul (α := E) (β := E) (1 : E) ((b : (a : F) → E) 1 : E)),
  Eq.{u_2 + 1} (α := E) ((algebraMap F E : (a : F) → E) (x * y) : E) ((b : (a : F) → E) x : E)
Tactic: rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy
Cleared hypotheses: hy