awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
i : σ
j : ι
⊢ (tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S) (X i ⊗ₜ[R] X j) =
    HMul.hMul (α := MvPolynomial (σ ⊕ ι) S) (X (Sum.inl i)) (X (Sum.inr j))

Tactic:
simp [tensorEquivSum]

Premises used: MvPolynomial.tensorEquivSum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
x : MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ S)
    (((↑(algebraTensorAlgEquiv R S) : S ⊗[R] MvPolynomial σ R ≃ₗ[S] MvPolynomial σ S) :
          (a : S ⊗[R] MvPolynomial σ R) → MvPolynomial σ S)
        (1 ⊗ₜ[R] x) :
      MvPolynomial σ S)
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R (MvPolynomial σ R) (MvPolynomial σ S)) :
          (a : MvPolynomial σ R) → MvPolynomial σ S)
        x :
      MvPolynomial σ S)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
⊢ Algebra.IsPushout R (MvPolynomial σ R) S (MvPolynomial σ S)

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.TensorProduct.Nontrivial
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
ha : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
inst_5 : IsDomain A
inst_6 : IsDomain B
⊢ IsDomain R

Tactic:
haveI := ha.isDomain _
-- Module: Mathlib.RingTheory.TensorProduct.Nontrivial
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
ha : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
inst_5 : IsDomain A
inst_6 : IsDomain B
this_1 : IsDomain R
FR : Type u_1 := FractionRing R
FA : Type u_2 := FractionRing A
FB : Type u_3 := FractionRing B
fa : FR →ₐ[R] FA :=
  IsFractionRing.liftAlgHom.{u_1, u_1, u_1, u_2} (R := R) (A := R) (K := FR) (L := FA) (g := ofId R FA) ⋯
fb : FR →ₐ[R] FB :=
  IsFractionRing.liftAlgHom.{u_1, u_1, u_1, u_3} (R := R) (A := R) (K := FR) (L := FB) (g := ofId R FB) ⋯
algInst : Algebra FR FA := fa.toAlgebra
algInst_1 : Algebra FR FB := fb.toAlgebra
this : CompatibleSMul FR R FA FB := ⋯
⊢ Nontrivial (A ⊗[R] B)

Tactic:
Algebra.TensorProduct.mapOfCompatibleSMul FR R R FA FB |>.comp
    (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R A FA) (IsScalarTower.toAlgHom R B FB))
    |>.toRingHom.domain_nontrivial

Premises used: Algebra.TensorProduct.map, IsScalarTower.toAlgHom, Algebra.TensorProduct.mapOfCompatibleSMul, AlgHom.toRingHom, RingHom.domain_nontrivial, AlgHom.comp
-- Module: Mathlib.RingTheory.TensorProduct.Nontrivial
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
ha : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
hb : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
inst_5 : IsDomain A
inst_6 : IsDomain B
this_1 : IsDomain R
FR : Type u_1 := FractionRing R
FA : Type u_2 := FractionRing A
FB : Type u_3 := FractionRing B
fa : FR →ₐ[R] FA :=
  IsFractionRing.liftAlgHom.{u_1, u_1, u_1, u_2} (R := R) (A := R) (K := FR) (L := FA) (g := ofId R FA) ⋯
fb : FR →ₐ[R] FB :=
  IsFractionRing.liftAlgHom.{u_1, u_1, u_1, u_3} (R := R) (A := R) (K := FR) (L := FB) (g := ofId R FB) ⋯
algInst : Algebra FR FA := fa.toAlgebra
algInst_1 : Algebra FR FB := fb.toAlgebra
this : CompatibleSMul FR R FA FB := ⋯
⊢ Nontrivial (A ⊗[R] B)

Tactic:
exact Algebra.TensorProduct.mapOfCompatibleSMul FR R R FA FB |>.comp
    (Algebra.TensorProduct.map (IsScalarTower.toAlgHom R A FA) (IsScalarTower.toAlgHom R B FB))
    |>.toRingHom.domain_nontrivial

Premises used: Algebra.TensorProduct.map, IsScalarTower.toAlgHom, Algebra.TensorProduct.mapOfCompatibleSMul, AlgHom.toRingHom, RingHom.domain_nontrivial, AlgHom.comp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        1 :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (1 : (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
y : A ⊗[R] ((i : ι) → B i)
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (0 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          0 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x : A
y : (i : ι) → B i
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) 0) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          0 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x : A
y : (i : ι) → B i
x_1 : A
y_1 : (i : ι) → B i
tmul :
  ∀ (j : ι),
    ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) (x_1 ⊗ₜ[R] y_1)) j =
      HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            (x ⊗ₜ[R] y) :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            (x_1 ⊗ₜ[R] y_1) :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        j
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) (x_1 ⊗ₜ[R] y_1)) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
ext j
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x : A
y : (i : ι) → B i
x_1 : A
y_1 : (i : ι) → B i
j : ι
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (HMul.hMul (α := A ⊗[R] ((i : ι) → B i)) (x ⊗ₜ[R] y) (x_1 ⊗ₜ[R] y_1)) j =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 ⊗ₜ[R] y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      j

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
x : A
y : (i : ι) → B i
x_1 y_1 : A ⊗[R] ((i : ι) → B i)
h :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y * x_1) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          x_1 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
h_1 :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y * y_1) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y_1 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x ⊗ₜ[R] y * (x_1 + y_1)) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x ⊗ₜ[R] y) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x_1 + y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp_all [mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
y x y_1 : A ⊗[R] ((i : ι) → B i)
h :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (x * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          x :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
h_1 :
  ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      (y_1 * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y_1 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
⊢ ((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
        (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
      ((x + y_1) * y) =
    HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          (x + y_1) :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
      (((piRightHom R S A B : A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
            (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
          y :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp_all [add_mul]

Premises used: add_mul
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((_root_.TensorProduct.piRightHom R S A B :
            A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        1 :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (1 : (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
⊢ ∀ (x y : A ⊗[R] ((i : ι) → B i)),
    ((_root_.TensorProduct.piRightHom R S A B :
            A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        (x * y) =
      HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((_root_.TensorProduct.piRightHom R S A B :
                A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            x :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((_root_.TensorProduct.piRightHom R S A B :
                A ⊗[R] ((i : ι) → B i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            y :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((_root_.TensorProduct.piRight R S A B :
            A ⊗[R] ((i : ι) → B i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        1 :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (1 : (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
⊢ ∀ (x y : A ⊗[R] ((i : ι) → B i)),
    ((_root_.TensorProduct.piRight R S A B :
            A ⊗[R] ((i : ι) → B i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        (x * y) =
      HMul.hMul (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) (β :=
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((_root_.TensorProduct.piRight R S A B :
                A ⊗[R] ((i : ι) → B i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            x :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
        (((_root_.TensorProduct.piRight R S A B :
                A ⊗[R] ((i : ι) → B i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
              (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
            y :
          (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst_7 : (i : ι) → Semiring (B i)
inst_8 : (i : ι) → Algebra.{u_1, u_5} R (B i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : A
f : (i : ι) → B i
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    (((piRight R S A B : A ⊗[R] ((i : ι) → B i) ≃ₐ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i)) :
          (a : A ⊗[R] ((i : ι) → B i)) → (i : ι) → A ⊗[R] B i)
        (x ⊗ₜ[R] f) :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
    fun (j : ι) ↦ (x ⊗ₜ[R] f j : TensorProduct.{u_1, u_3, u_5} R A (B j))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : A
y : ι → R
⊢ Eq (α := ι → A)
    (((piScalarRight R S A ι : A ⊗[R] (ι → R) ≃ₐ[S] ι → A) : (a : A ⊗[R] (ι → R)) → ι → A) (x ⊗ₜ[R] y) : ι → A)
    fun (i : ι) ↦ y i • x

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.TensorProduct.Pi
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : A
y : ι → R
i : ι
⊢ ((piScalarRight R S A ι : A ⊗[R] (ι → R) ≃ₐ[S] ι → A) : (a : A ⊗[R] (ι → R)) → ι → A) (x ⊗ₜ[R] y) i = y i • x

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl