-- 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))
⊢ 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 : 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)
Tactic: induction c
Cleared hypotheses: c