-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Pi (goal)
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)
zero :
  ((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))
tmul :
  ∀ (x : A) (y_1 : (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)
        (x ⊗ₜ[R] 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 ⊗ₜ[R] 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) =
    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))
have add : ∀ (x y_1 : 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)
        (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)) →
    ((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: induction x
Cleared hypotheses: x