-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
c : (↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u))
h :
  Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
          (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
          (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
          (Under.Hom.right
            (AlgHom.toUnder
              (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u))
                (Pi.evalAlgHom (↑R : Type u) (fun (j : ι) ↦ (↑(P j).right : Type u)) i)))) :
        (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
          (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
      0)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
          (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
          (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
          (Under.Hom.right
            (CategoryStruct.comp (Y := S.mkUnder ((i : ι) → (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
              (Iso.hom
                (AlgEquiv.toUnder
                  (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
                    (↑(P i).right : Type u))))
              (AlgHom.toUnder
                (Pi.evalAlgHom (↑S : Type u) (fun (i : ι) ↦ (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))
                  i)))) :
        (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
          (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
      0)
⊢ Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (AlgHom.toUnder
                (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u))
                  (Pi.evalAlgHom (↑R : Type u) (fun (j : ι) ↦ (↑(P j).right : Type u)) i)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        c :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (CategoryStruct.comp (Y := S.mkUnder ((i : ι) → (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
                (Iso.hom
                  (AlgEquiv.toUnder
                    (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
                      (↑(P i).right : Type u))))
                (AlgHom.toUnder
                  (Pi.evalAlgHom (↑S : Type u) (fun (i : ι) ↦ (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))
                    i)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        c :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
have h₁ : ∀ (x : (↑S : Type u)) (y : (i : ι) → (↑(P i).right : Type u)),
  Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (AlgHom.toUnder
                (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u))
                  (Pi.evalAlgHom (↑R : Type u) (fun (j : ι) ↦ (↑(P j).right : Type u)) i)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        (x ⊗ₜ[(↑R : Type u)] y) :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (CategoryStruct.comp (Y := S.mkUnder ((i : ι) → (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
                (Iso.hom
                  (AlgEquiv.toUnder
                    (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
                      (↑(P i).right : Type u))))
                (AlgHom.toUnder
                  (Pi.evalAlgHom (↑S : Type u) (fun (i : ι) ↦ (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))
                    i)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        (x ⊗ₜ[(↑R : Type u)] y) :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
Tactic: induction c
Cleared hypotheses: c