awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        x :
      ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
      ⨂[R] (i : ι), A i)
have rw : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        x :
      ⨂[R] (i : ι), A i) =
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      1)
Tactic: rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
      (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          x :
        ⨂[R] (i : ι), A i) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
      ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        1)
have change : r • (1 * x) = r • (x * 1)
Tactic: change r • (1 * x) = r • (x * 1)
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • (1 * x) = r • (x * 1)
have rw : r • (1 * x) = r • x
Tactic: rw [mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
rw : r • (1 * x) = r • x
⊢ r • (1 * x) = r • (x * 1)
have rw₁ : r • x = r • x
Tactic: rw [mul_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x
have change : r • x =
  (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
          (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
        (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
      (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
    x
Tactic: change _ = mul _ _
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x =
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
            (HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1) :
          (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
        (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
      x
have rw : r • x =
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
    (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        x :
      ⨂[R] (i : ι), A i)
Tactic: rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r
      (((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) 1 :
            (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
          x :
        ⨂[R] (i : ι), A i)
have change : r • x = r • (1 * x)
Tactic: change _ = r • (1 * x)
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ r • x = r • (1 * x)
have rw : r • x = r • x
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
⊢ Eq (α := ⨂[R] (i : ι), A i) ((algebraMap R' (⨂[R] (i : ι), A i) : (a : R') → ⨂[R] (i : ι), A i) r : ⨂[R] (i : ι), A i)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
        (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r)) :
      ⨂[R] (i : ι), A i)
have change : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
    (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
Tactic: change r • tprod R 1 = _
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
⊢ Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
have rw : Pi.mulSingle (M := A) i (HSMul.hSMul (β := A i) r 1) = update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
Tactic: rw [Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (hypothesis)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have this : Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
  update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
Tactic: have : Pi.mulSingle i (algebraMap R' (A i) r) = update (fun i ↦ 1) i (r • 1) := by
    rw [Algebra.algebraMap_eq_smul_one]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
    (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
rw :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw₁ : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
    (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) (HSMul.hSMul (β := R) r 1) 1))
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
rw :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
rw₁ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) (HSMul.hSMul (β := R) r 1) 1))
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw₂ : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (update (β := A) (fun (i : ι) ↦ 1) i 1))
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
rw :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
rw₁ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) (HSMul.hSMul (β := R) r 1) 1))
rw₂ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (update (β := A) (fun (i : ι) ↦ 1) i 1))
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw₃ : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1) (⨂ₜ[R] (i : ι), 1)
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
rw :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
rw₁ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) (HSMul.hSMul (β := R) r 1) 1))
rw₂ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (update (β := A) (fun (i : ι) ↦ 1) i 1))
rw₃ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1) (⨂ₜ[R] (i : ι), 1)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw₄ : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (⨂ₜ[R] (i : ι), 1)
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
r : R'
i : ι
inst_7 : DecidableEq ι
this :
  Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
rw :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1))
rw₁ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) (HSMul.hSMul (β := R) r 1) 1))
rw₂ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1)
      ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (update (β := A) (fun (i : ι) ↦ 1) i 1))
rw₃ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (HSMul.hSMul (β := R) r 1) (⨂ₜ[R] (i : ι), 1)
rw₄ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (⨂ₜ[R] (i : ι), 1)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) =
    (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (Pi.mulSingle (M := A) i ((algebraMap R' (A i) : (a : R') → A i) r))
have rw₅ : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (⨂ₜ[R] (x : ι), 1) = HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (⨂ₜ[R] (i : ι), 1)
Tactic: rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
inst_7 : DecidableEq ι
i : ι
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
      (((MonoidHom.mulSingle A i : A i →* (i : ι) → A i) : (a : A i) → (i : ι) → A i) 1))
    1
have simp : Eq (α := ⨂[R] (i : ι), A i) ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) 1
Tactic: simp only [map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R'
inst_1 : CommSemiring R
inst_2 : (i : ι) → Semiring (A i)
inst_3 : Algebra R' R
inst_4 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} R' (A i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_2, u_3, u_4} R' R (A i)
inst_7 : DecidableEq ι
i : ι
r : R
⊢ tprodCoeff R (s := A) 1
      (((MonoidHom.mulSingle A i : A i →* (i : ι) → A i) : (a : A i) → (i : ι) → A i)
        ((algebraMap R (A i) : (a : R) → A i) r : A i)) =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (tprodCoeff R (s := A) 1 1)
have rw : tprodCoeff R (s := A) (HSMul.hSMul (β := R) r 1) 1 = HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (tprodCoeff R (s := A) 1 1)
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← Pi.one_apply, MonoidHom.mulSingle_apply, Pi.mulSingle,
      smul_tprodCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
x y : ⨂[R] (i : ι), A i
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) x :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        y :
      ⨂[R] (i : ι), A i)
    ((((mul (A := A) : (a : ⨂[R] (i : ι), A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) y :
            (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) :
          (a : ⨂[R] (i : ι), A i) → ⨂[R] (i : ι), A i)
        x :
      ⨂[R] (i : ι), A i)
have suffices : Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (mul (A := A))
  (LinearMap.flip (mul (A := A)))
Tactic: suffices mul (R := R) (A := A) = mul.flip from
    DFunLike.congr_fun (DFunLike.congr_fun this x) y
-- Lean 4 proof step from Mathlib.RingTheory.PiTensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
x y : ⨂[R] (i : ι), A i
⊢ Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i) (mul (A := A))
    (LinearMap.flip (mul (A := A)))
have H : ∀ (x y : (i : ι) → A i),
  Eq (α := ⨂[R] (i : ι), A i)
    ((LinearMap.compMultilinearMap (M₁ := A)
            ((LinearMap.compMultilinearMap (M₁ := A) (mul (A := A)) (tprod R (s := A)) :
                (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              x)
            (tprod R (s := A)) :
          (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
        y :
      ⨂[R] (i : ι), A i)
    ((LinearMap.compMultilinearMap (M₁ := A)
            ((LinearMap.compMultilinearMap (M₁ := A) (LinearMap.flip (mul (A := A))) (tprod R (s := A)) :
                (a : (i : ι) → A i) → (⨂[R] (i : ι), A i) →ₗ[R] ⨂[R] (i : ι), A i)
              x)
            (tprod R (s := A)) :
          (a : (i : ι) → A i) → ⨂[R] (i : ι), A i)
        y :
      ⨂[R] (i : ι), A i)
Tactic: ext x y