awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
rw :
  Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
    Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
      Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
        Under.homMk
          (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
          ⋯
⊢ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
      Under.homMk
        (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
        ⋯

Tactic:
rw [← cancel_epi (tensorProdObjIsoPushoutObj S A).inv]

Premises used: CategoryTheory.cancel_epi, CommRingCat.tensorProdObjIsoPushoutObj, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
          Under.homMk
            (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
              (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
            ⋯)
⊢ Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B) =
    Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
      Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
        Under.homMk
          (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
            (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
          ⋯

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)
h₁ :
  pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)
⊢ Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
          Under.homMk
            (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
              (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
            ⋯)

Tactic:
apply pushout.hom_ext

Premises used: CategoryTheory.Limits.pushout.hom_ext
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
⊢ pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)

Tactic:
rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Under.Hom.right, CommRingCat.tensorProdObjIsoPushoutObj, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  ∀ (x : (↑A.right : Type u)),
    Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
      ((Hom.hom
              ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                  Under.Hom.right
                    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                      (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
                Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
            (a : (↑A.right : Type u)) →
              (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
          x :
        (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
      ((Hom.hom
              ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                  Under.Hom.right
                    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                      Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                        Under.homMk
                          (pushout.desc
                            (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                            (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                          ⋯)) ≫
                Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
            (a : (↑A.right : Type u)) →
              (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
          x :
        (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
⊢ (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
x : (↑A.right : Type u)
⊢ Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑A.right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                      Under.homMk
                        (pushout.desc
                          (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                        ⋯)) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑A.right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))

Tactic:
simp [mkUnder_right]

Premises used: CommRingCat.mkUnder_right
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
⊢ pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)

Tactic:
rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Under.Hom.right, CommRingCat.tensorProdObjIsoPushoutObj, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  ∀ (x : (↑S : Type u)),
    Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
      ((Hom.hom
              ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                  Under.Hom.right
                    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                      (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
                Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
            (a : (↑(of (↑S : Type u)) : Type u)) →
              (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
          x :
        (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
      ((Hom.hom
              ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                  Under.Hom.right
                    (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                      Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                        Under.homMk
                          (pushout.desc
                            (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                            (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                          ⋯)) ≫
                Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
            (a : (↑(of (↑S : Type u)) : Type u)) →
              (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
          x :
        (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
⊢ (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))

Tactic:
ext (x : S)
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
x : (↑S : Type u)
⊢ Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑(of (↑S : Type u)) : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                      Under.homMk
                        (pushout.desc
                          (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                        ⋯)) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑(of (↑S : Type u)) : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))

Tactic:
simp [mkUnder_right]

Premises used: CommRingCat.mkUnder_right
-- Module: Mathlib.Algebra.Category.Ring.Under.Basic
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A : Under R
⊢ Eq (α := (R.tensorProd S).obj A ≅ Functor.obj (Under.pushout (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) A)
    (Iso.app (R.tensorProdIsoPushout S) A) (tensorProdObjIsoPushoutObj S A)

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.isoMk, CommRingCat.mkUnder, CategoryTheory.Under.mk, CategoryTheory.Comma.isoMk, CategoryTheory.Under.isoMk, CategoryTheory.Under, CategoryTheory.Under.Hom, CategoryTheory.StructuredArrow.mk, CategoryTheory.Iso.app, CommRingCat.tensorProdObjIsoPushoutObj, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
dsimp :
  Eq.{u + 1} (α :=
    S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u))) ⟶
      S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
    (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)))
    (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)))
⊢ Eq (α :=
    Cone.pt (F := Discrete.functor fun (i : ι) ↦ S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
        (tensorProductFan S P) ⟶
      S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
    (Fan.proj (tensorProductFan S P) i)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := Discrete.functor fun (i : ι) ↦ S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
        (tensorProductFan' S P))
      (Iso.hom
        (AlgEquiv.toUnder
          (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
            (↑(P i).right : Type u))))
      (Fan.proj (tensorProductFan' S P) i))

Tactic:
dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']

Premises used: CommRingCat.Under.tensorProductFan', CommRingCat.Under.tensorProductFan, CategoryTheory.Limits.fan_mk_proj, CategoryTheory.Limits.Fan.mk_pt
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
⊢ 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:
simp only [map_zero, Under.comp_right]

Premises used: map_zero, CategoryTheory.Under.comp_right