-- Lean 4 proof step from Mathlib.Algebra.Algebra.Equiv (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
e : R ≃ₗ[R] A
x : A
rw :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₁ :
  HMul.hMul (α := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₂ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) (β := A)
        ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) :
          A)
        ((e : (a : R) → A) 1 : A)) =
    x
rw₃ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A)
        ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) ((e : (a : R) → A) 1 : A)) =
    x
rw₄ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            1) :
        A) =
    x
rw₅ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A)
          (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R)
            (1 : R)) :
        A) =
    x
rw₆ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      ((e : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A) =
    x
rw₇ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
      (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) =
    x
rw₈ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A)
        ((e : (a : R) → A) 1 : A) *
      x =
    x
rw₉ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((e.symm : (a : A) → R) 1 : R) ((e : (a : R) → A) 1 : A) * x = x
rw₁₀ : HMul.hMul (α := A) ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A) x = x
rw₁₁ :
  HMul.hMul (α := A) ((e : (a : R) → A) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A) x = x
rw₁₂ : HMul.hMul (α := A) ((e : (a : R) → A) ((e.symm : (a : A) → R) 1 : R) : A) x = x
⊢ HMul.hMul (α := A) (β := A)
      ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
      ((e : (a : R) → A) (HSMul.hSMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) 1) : A) =
    x
have rw₁₃ : 1 * x = x
Tactic: rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]