-- 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)
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))
⊢ 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 y : (↑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))
          x :
        (↑(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 :
        (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).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))
            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))
            y :
          (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).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 + 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 + y) :
          (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
Tactic: induction c
Cleared hypotheses: c