awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PiTensorProduct
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 s : R'
e_a : 1 = HMul.hMul (α := ⨂[R] (i : ι), A i) 1 1
⊢ Eq (α := ⨂[R] (i : ι), A i) 1
    (((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)
      1)

Tactic:
change (1 : ⨂[R] i, A i) = 1 * 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.PiTensorProduct
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 s : R'
e_a e_a₁ : Eq (α := ⨂[R] (i : ι), A i) 1 1
⊢ 1 = HMul.hMul (α := ⨂[R] (i : ι), A i) 1 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.PiTensorProduct
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)
⊢ HSMul.hSMul (α := R') (β := ⨂[R] (i : ι), A i) 0 1 = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PiTensorProduct
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)
⊢ ∀ (x y : R'),
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) (x + y) 1 =
      HSMul.hSMul (β := ⨂[R] (i : ι), A i) x 1 + HSMul.hSMul (β := ⨂[R] (i : ι), A i) y 1

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.PiTensorProduct
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
simp : HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x = x * HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1
⊢ HMul.hMul (α := ⨂[R] (i : ι), A i)
      ((({ toFun := fun (x : R') ↦ HSMul.hSMul (β := ⨂[R] (i : ι), A i) x 1, map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ } :
              R' →+* ⨂[R] (i : ι), A i) :
            (a : R') → ⨂[R] (i : ι), A i)
          r :
        ⨂[R] (i : ι), A i)
      x =
    HMul.hMul (β := ⨂[R] (i : ι), A i) x
      ((({ toFun := fun (x : R') ↦ HSMul.hSMul (β := ⨂[R] (i : ι), A i) x 1, map_one' := ⋯, map_mul' := ⋯,
                map_zero' := ⋯, map_add' := ⋯ } :
              R' →+* ⨂[R] (i : ι), A i) :
            (a : R') → ⨂[R] (i : ι), A i)
          r :
        ⨂[R] (i : ι), A i)

Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: OneHom.coe_mk, MonoidHom.coe_mk, RingHom.coe_mk
-- Module: Mathlib.RingTheory.PiTensorProduct
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
change :
  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)
⊢ HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x = x * HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1

Tactic:
change mul _ _ = mul _ _

Premises used: PiTensorProduct.mul, DFunLike.coe
-- Module: Mathlib.RingTheory.PiTensorProduct
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 :
  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)
⊢ 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)

Tactic:
rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.map_smul_of_tower
-- Module: Mathlib.RingTheory.PiTensorProduct
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
change : r • (1 * x) = r • (x * 1)
⊢ 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:
change r • (1 * x) = r • (x * 1)

Premises used: HMul.hMul, OfNat.ofNat
-- Module: Mathlib.RingTheory.PiTensorProduct
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
rw₁ rw₂ : r • x = r • x
⊢ r • (1 * x) = r • (x * 1)

Tactic:
rw [mul_one, one_mul]

Premises used: mul_one, one_mul
-- Module: Mathlib.RingTheory.PiTensorProduct
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
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
⊢ r • x = HSMul.hSMul (β := ⨂[R] (i : ι), A i) r 1 * x

Tactic:
change _ = mul _ _

Premises used: PiTensorProduct.mul, DFunLike.coe
-- Module: Mathlib.RingTheory.PiTensorProduct
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 • 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)
⊢ 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:
rw [LinearMap.map_smul_of_tower, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, LinearMap.map_smul_of_tower
-- Module: Mathlib.RingTheory.PiTensorProduct
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
change : r • x = r • (1 * x)
⊢ 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:
change _ = r • (1 * x)

Premises used: HMul.hMul, OfNat.ofNat
-- Module: Mathlib.RingTheory.PiTensorProduct
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 rw₁ : r • x = r • x
⊢ r • x = r • (1 * x)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.RingTheory.PiTensorProduct
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 ι
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))
⊢ 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)

Tactic:
change r • tprod R 1 = _

Premises used: PiTensorProduct.tprod, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PiTensorProduct
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 ι
rw :
  Pi.mulSingle (M := A) i (HSMul.hSMul (β := A i) r 1) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)
⊢ 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:
rw [Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.PiTensorProduct
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 (HSMul.hSMul (β := A i) r 1) =
    update (β := A) (fun (i : ι) ↦ 1) i (HSMul.hSMul (β := A i) r 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PiTensorProduct
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)

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
-- Module: Mathlib.RingTheory.PiTensorProduct
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)
rw₅ rw₆ :
  HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (⨂ₜ[R] (x : ι), 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))

Tactic:
rw [this, ← smul_one_smul R r (1 : A i), MultilinearMap.map_update_smul, update_eq_self,
    smul_one_smul, Pi.one_def]

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, smul_one_smul, Pi.one_def, OfNat.ofNat
-- Module: Mathlib.RingTheory.PiTensorProduct
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 : ι
simp : Eq (α := ⨂[R] (i : ι), A i) ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) 1
⊢ 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

Tactic:
simp only [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.PiTensorProduct
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) 1) 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.PiTensorProduct
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 : ι
a a' : 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) (a * a')) =
    HMul.hMul (α := ⨂[R] (i : ι), A i) (β := ⨂[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) a) :
        ⨂[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) a') :
        ⨂[R] (i : ι), A i)

Tactic:
simp [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.PiTensorProduct
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
rw :
  tprodCoeff R (s := A) (HSMul.hSMul (β := R) r 1) 1 =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (tprodCoeff R (s := A) 1 1)
⊢ 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)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← Pi.one_apply, MonoidHom.mulSingle_apply, Pi.mulSingle,
      smul_tprodCoeff]

Premises used: Pi.one_apply, MonoidHom.mulSingle_apply, Algebra.algebraMap_eq_smul_one, PiTensorProduct.smul_tprodCoeff, Pi.mulSingle
-- Module: Mathlib.RingTheory.PiTensorProduct
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) (HSMul.hSMul (β := R) r 1) 1 =
    HSMul.hSMul (β := ⨂[R] (i : ι), A i) r (tprodCoeff R (s := A) 1 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PiTensorProduct
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)
S : Type u_5
inst_7 : Semiring S
inst_8 : Algebra R S
f : MultilinearMap R A S
one : Eq.{u_5 + 1} (α := S) ((f : (a : (i : ι) → A i) → S) 1 : S) (1 : S)
mul :
  ∀ (x y : (i : ι) → A i),
    (f : (a : (i : ι) → A i) → S) (x * y) =
      HMul.hMul (α := S) (β := S) ((f : (a : (i : ι) → A i) → S) x : S) ((f : (a : (i : ι) → A i) → S) y : S)
⊢ Eq.{u_5 + 1} (α := S)
    ((((lift (s := A) : (a : MultilinearMap R A S) → (⨂[R] (i : ι), A i) →ₗ[R] S) f : (⨂[R] (i : ι), A i) →ₗ[R] S) :
          (a : ⨂[R] (i : ι), A i) → S)
        ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) 1) :
      S)
    (1 : S)

Tactic:
simp [one]
-- Module: Mathlib.RingTheory.PiTensorProduct
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)
S : Type u_5
inst_7 : Semiring S
inst_8 : Algebra R S
f : MultilinearMap R A S
one : Eq.{u_5 + 1} (α := S) ((f : (a : (i : ι) → A i) → S) 1 : S) (1 : S)
mul :
  ∀ (x y : (i : ι) → A i),
    (f : (a : (i : ι) → A i) → S) (x * y) =
      HMul.hMul (α := S) (β := S) ((f : (a : (i : ι) → A i) → S) x : S) ((f : (a : (i : ι) → A i) → S) y : S)
⊢ Eq (α := (⨂[R] (i : ι), A i) →ₗ[R] (⨂[R] (i : ι), A i) →ₗ[R] S)
    (LinearMap.compr₂ (LinearMap.mul R (⨂[R] (i : ι), A i))
      ((lift (s := A) : (a : MultilinearMap R A S) → (⨂[R] (i : ι), A i) →ₗ[R] S) f))
    (LinearMap.compl₂ (σ₄₂ := RingHom.id R)
      (LinearMap.mul R S ∘ₗ (lift (s := A) : (a : MultilinearMap R A S) → (⨂[R] (i : ι), A i) →ₗ[R] S) f)
      ((lift (s := A) : (a : MultilinearMap R A S) → (⨂[R] (i : ι), A i) →ₗ[R] S) f))

Tactic:
aesop
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
κ : Type u_5
s : Finset κ
x : κ → (i : ι) → A i
hx : (↑s : Set κ).Pairwise (Commute on x)
⊢ Eq (α := ⨂[R] (i : ι), A i)
    ((tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (s.noncommProd x hx) : ⨂[R] (i : ι), A i)
    (s.noncommProd (fun (k : κ) ↦ (tprod R (s := A) : (a : (i : ι) → A i) → ⨂[R] (i : ι), A i) (x k)) ⋯ :
      ⨂[R] (i : ι), A i)

Tactic:
Finset.map_noncommProd s x _ (tprodMonoidHom R)

Premises used: PiTensorProduct.tprodMonoidHom, Finset.map_noncommProd, PiTensorProduct.tprodCoeff, AddCon.toQuotient
-- Module: Mathlib.RingTheory.PiTensorProduct
Goal:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst : CommSemiring R
inst_1 : (i : ι) → Semiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
S : Type u_5
inst_3 : Finite ι
inst_4 : DecidableEq ι
inst_5 : Semiring S
inst_6 : Algebra R S
f g : (⨂[R] (i : ι), A i) →ₐ[R] S
h : ∀ (i : ι), f.comp (singleAlgHom (A := A) i) = g.comp (singleAlgHom (A := A) i)
⊢ f = g

Tactic:
AlgHom.toLinearMap_injective <| PiTensorProduct.ext <| MultilinearMap.ext fun x =>
    suffices f.toMonoidHom.comp (tprodMonoidHom R) = g.toMonoidHom.comp (tprodMonoidHom R) from
      DFunLike.congr_fun this x
    MonoidHom.pi_ext fun i xi => DFunLike.congr_fun (h i) xi

Premises used: DFunLike.congr_fun, MonoidHom.pi_ext, AlgHom.toLinearMap_injective, MultilinearMap.ext, PiTensorProduct.ext