-- 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)
y : A ⊗[R] ((i : ι) → B i)
x : A
y_1 : (i : ι) → B i
tmul :
  ((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_1) 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_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)
          0 :
        (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
tmul₁ :
  ∀ (x_1 : 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_1) (x_1 ⊗ₜ[R] 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)
            (x_1 ⊗ₜ[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 ⊗ₜ[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))
have tmul₂ : ∀ (x_1 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)
        (x ⊗ₜ[R] y_1 * 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_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_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_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 ⊗ₜ[R] y_1 * (x_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)
              (x_1 + y) :
            (i : ι) → TensorProduct.{u_1, u_3, u_5} R A (B i))
Tactic: induction y
Cleared hypotheses: y