awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A)
⊢ (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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)
have rw₁ : (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
  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) ((e.symm : (a : A) → R) 1 : R) : A)
Tactic: rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
-- 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 :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A)
rw₁ :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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) ((e.symm : (a : A) → R) 1 : R) : A)
⊢ (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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)
have rw₂ : (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
  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)
    (1 : A)
Tactic: rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
-- 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 :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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) (HMul.hMul (α := R) (β := R) ((e.symm : (a : A) → R) 1 : R) (1 : R)) : A)
rw₁ :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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) ((e.symm : (a : A) → R) 1 : R) : A)
rw₂ :
  (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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)
      (1 : A)
⊢ (algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) =
    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)
have rw₃ : Eq.{u_2 + 1} (α := A)
  ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
  ((algebraMap R A : (a : R) → A) ((e.symm : (a : A) → R) (HMul.hMul (α := A) ((e : (a : R) → A) 1 : A) x) : R) : A)
Tactic: rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
-- 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
⊢ 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 : 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
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]
-- 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
⊢ 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₁ : 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
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]
-- 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
⊢ 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₂ : 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
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]
-- 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
⊢ 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₃ : 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
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]
-- 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
⊢ 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₄ : 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
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]
-- 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
⊢ 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₅ : 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
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]
-- 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
⊢ 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₆ : 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
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]
-- 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
⊢ 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₇ : 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
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]
-- 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
⊢ 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₈ : 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
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]