-- 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 : (i : ι) → CommSemiring (A i)
inst_2 : (i : ι) → Algebra.{u_3, u_4} R (A i)
inst_3 : Fintype ι
toFun : (⨂[R] (i : ι), R) →ₗ[R] R :=
  (lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
    (MultilinearMap.mkPiAlgebra R ι R)
this_1 : IsScalarTower R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
this : SMulCommClass R (⨂[R] (x : ι), R) (⨂[R] (x : ι), R) := ⋯
H :
  (toFun : (a : ⨂[R] (i : ι), R) → R)
      ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R)
          (HMul.hMul (α := (i : ι) → R) (fun (x : ι) ↦ 1) fun (x : ι) ↦ 1) :
        ⨂[R] (i : ι), R) =
    HMul.hMul (α := R) (β := R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
H₁ :
  (((lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
            (MultilinearMap.mkPiAlgebra R ι R) :
          (⨂[R] (i : ι), R) →ₗ[R] R) :
        (a : ⨂[R] (i : ι), R) → R)
      ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R)
          (HMul.hMul (α := (i : ι) → R) (fun (x : ι) ↦ 1) fun (x : ι) ↦ 1) :
        ⨂[R] (i : ι), R) =
    HMul.hMul (α := R) (β := R)
      ((((lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
                (MultilinearMap.mkPiAlgebra R ι R) :
              (⨂[R] (i : ι), R) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
      ((((lift (s := fun (x : ι) ↦ R) : (a : MultilinearMap R (fun (x : ι) ↦ R) R) → (⨂[R] (i : ι), R) →ₗ[R] R)
                (MultilinearMap.mkPiAlgebra R ι R) :
              (⨂[R] (i : ι), R) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
H₂ :
  (MultilinearMap.mkPiAlgebra R ι R : (a : (i : ι) → R) → R)
      (HMul.hMul (α := (i : ι) → R) (fun (x : ι) ↦ 1) fun (x : ι) ↦ 1) =
    HMul.hMul (α := R) (β := R) ((MultilinearMap.mkPiAlgebra R ι R : (a : (i : ι) → R) → R) fun (x : ι) ↦ 1 : R)
      ((MultilinearMap.mkPiAlgebra R ι R : (a : (i : ι) → R) → R) fun (x : ι) ↦ 1 : R)
H₃ :
  ∏ i : ι, HMul.hMul (α := (i : ι) → R) (β := (i : ι) → R) (fun (x : ι) ↦ 1) (fun (x : ι) ↦ 1) i =
    HMul.hMul (α := R) (∏ x : ι, 1) (∏ x : ι, 1)
H₄ : ∏ x : ι, HMul.hMul (α := R) 1 1 = HMul.hMul (α := R) (∏ x : ι, 1) (∏ x : ι, 1)
⊢ (toFun : (a : ⨂[R] (i : ι), R) → R)
      (HMul.hMul (α := ⨂[R] (i : ι), R)
        ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1)
        ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1)) =
    HMul.hMul (α := R) (β := R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)
      ((toFun : (a : ⨂[R] (i : ι), R) → R)
          ((tprod R (s := fun (i : ι) ↦ R) : (a : (i : ι) → R) → ⨂[R] (i : ι), R) fun (x : ι) ↦ 1) :
        R)

Tactic:
simp_rw [tprod_mul_tprod, toFun, lift.tprod, MultilinearMap.mkPiAlgebra_apply,
          Pi.mul_apply, Finset.prod_mul_distrib]

Premises used: PiTensorProduct.lift.tprod, MultilinearMap.mkPiAlgebra_apply, Finset.prod_mul_distrib, Pi.mul_apply, PiTensorProduct.tprod_mul_tprod