awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
simp :
  Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) a)) :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) b)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))
⊢ LE.le (α := Subring (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
    (Subring.map (R := (↑X : Type u))
      (Hom.hom
        (Iso.inv
          (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
            ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)))
      ⊤)
    (Subring.closure
      (Set.image (α := (↑X : Type u))
          (⇑(Hom.hom
                (Iso.inv
                  (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                    ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H))) :
            (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
          (Set.range (ι := (↑A : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) a) :
              (a : (↑A : Type u)) → (↑X : Type u))) ∪
        Set.image (α := (↑X : Type u))
          (⇑(Hom.hom
                (Iso.inv
                  (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
                    ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H))) :
            (a : (↑X : Type u)) → (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u))
          (Set.range (ι := (↑B : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) b) :
              (a : (↑B : Type u)) → (↑X : Type u)))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, ← Set.range_comp, ← RingHom.coe_comp]

Premises used: Set.range_comp, AlgHom.toRingHom_eq_coe, RingHom.coe_comp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
rw :
  Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑Algebra.TensorProduct.includeLeftRingHom :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑(↑Algebra.TensorProduct.includeRight : (↑B : Type u) →+* (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) a)) :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑((Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv).comp
                (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) b)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))

Tactic:
rw [← hom_comp, ← hom_comp, IsPushout.inl_isoIsPushout_inv, IsPushout.inr_isoIsPushout_inv,
    hom_ofHom, hom_ofHom]

Premises used: CategoryTheory.IsPushout.inl_isoIsPushout_inv, CommRingCat.hom_comp, CategoryTheory.IsPushout.inr_isoIsPushout_inv, CommRingCat.hom_ofHom
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑Algebra.TensorProduct.includeLeftRingHom :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑(↑Algebra.TensorProduct.includeRight : (↑B : Type u) →+* (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))

Tactic:
le_top.trans (Algebra.TensorProduct.closure_range_union_range_eq_top R A B).ge

Premises used: Eq.ge, CommRingCat.carrier, Set.Mem, Quotient, le_top, TensorProduct, LE.le.trans, AddCon.Quotient, Algebra.TensorProduct.closure_range_union_range_eq_top
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R A B X : CommRingCat
f : R ⟶ A
g : R ⟶ B
a : A ⟶ X
b : B ⟶ X
H : IsPushout f g a b
algInst : Algebra (↑R : Type u) (↑A : Type u) := (Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑B : Type u) := (Hom.hom g).toAlgebra
e : (↑(of ((↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u))) : Type u) ≃+* (↑X : Type u) :=
  Iso.commRingCatIsoToRingEquiv
    (IsPushout.isoIsPushout A B (inl := ofHom Algebra.TensorProduct.includeLeftRingHom) (inr :=
      ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)) ⋯ H)
⊢ Subring.map (Hom.hom (IsPushout.isoIsPushout A B ⋯ H).inv) ⊤ ≤
    Subring.closure
      (Set.range (ι := (↑A : Type u))
          (⇑Algebra.TensorProduct.includeLeftRingHom :
            (a : (↑A : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) ∪
        Set.range (ι := (↑B : Type u))
          (⇑(↑Algebra.TensorProduct.includeRight : (↑B : Type u) →+* (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)) :
            (a : (↑B : Type u)) → (↑A : Type u) ⊗[(↑R : Type u)] (↑B : Type u)))

Tactic:
exact le_top.trans (Algebra.TensorProduct.closure_range_union_range_eq_top R A B).ge

Premises used: Eq.ge, CommRingCat.carrier, le_top, LE.le.trans, Algebra.TensorProduct.closure_range_union_range_eq_top
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
⊢ (A.coproductCocone B).inl = ofHom (AlgHom.toRingHom (R := ℤ) Algebra.TensorProduct.includeLeft)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
⊢ (A.coproductCocone B).inr = ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)
x_1 : (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)
⊢ Commute (S :=
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u))
    (((Hom.hom s.inl).toIntAlgHom :
          (a : (↑((pair A B).obj { as := WalkingPair.left }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))
    (((Hom.hom s.inr).toIntAlgHom :
          (a : (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
        x_1 :
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))

Tactic:
apply Commute.all

Premises used: Commute.all
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
j : WalkingPair
left :
  Eq (α := Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
    (s.ι.app { as := WalkingPair.left })
right :
  Eq (α := Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
    (s.ι.app { as := WalkingPair.right })
⊢ Eq (α := Functor.obj (pair A B) { as := j : Discrete WalkingPair } ⟶ s.pt)
    ((A.coproductCocone B).ι.app { as := j } ≫
      ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
    (s.ι.app { as := j })

Tactic:
cases j
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
left :
  ∀ (a : (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom
              ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
                ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                          (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u)))) :
            (a : (↑((pair A B).obj { as := WalkingPair.left }) : Type u)) → (↑s.pt : Type u))
          a :
        (↑s.pt : Type u))
      ((Hom.hom (s.ι.app { as := WalkingPair.left }) :
            (a : (↑((pair A B).obj { as := WalkingPair.left }) : Type u)) → (↑s.pt : Type u))
          a :
        (↑s.pt : Type u))
⊢ Eq (α := Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
      ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
    (s.ι.app { as := WalkingPair.left })

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
right :
  ∀ (a : (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)),
    Eq (α := (↑s.pt : Type u))
      ((Hom.hom
              ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
                ofHom
                  (AlgHom.toRingHom
                    (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                          (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                              { as := WalkingPair.left : Discrete WalkingPair }) :
                          Type u)))) :
            (a : (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) → (↑s.pt : Type u))
          a :
        (↑s.pt : Type u))
      ((Hom.hom (s.ι.app { as := WalkingPair.right }) :
            (a : (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) → (↑s.pt : Type u))
          a :
        (↑s.pt : Type u))
⊢ Eq (α := Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
      ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
    (s.ι.app { as := WalkingPair.right })

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
a : (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            ((A.coproductCocone B).ι.app { as := WalkingPair.left } ≫
              ofHom
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u)))) :
          (a : (↑((pair A B).obj { as := WalkingPair.left }) : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))
    ((Hom.hom (s.ι.app { as := WalkingPair.left }) :
          (a : (↑((pair A B).obj { as := WalkingPair.left }) : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
a : (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((Hom.hom
            ((A.coproductCocone B).ι.app { as := WalkingPair.right } ≫
              ofHom
                (AlgHom.toRingHom
                  (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                    (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                            { as := WalkingPair.left : Discrete WalkingPair }) :
                        Type u)))) :
          (a : (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))
    ((Hom.hom (s.ι.app { as := WalkingPair.right }) :
          (a : (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
m : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →+* (↑s.pt : Type u)
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
hf :
  Hom.hom { hom' := m } =
    Hom.hom
      (ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))
⊢ { hom' := m } =
    ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
          (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
              (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u)))

Tactic:
apply CommRingCat.hom_ext

Premises used: CommRingCat.hom_ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
m : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →+* (↑s.pt : Type u)
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
hf :
  RingHom.toIntAlgHom (Hom.hom { hom' := m }) =
    (Hom.hom
        (ofHom
          (AlgHom.toRingHom
            (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
              (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                  (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
                (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                      { as := WalkingPair.left : Discrete WalkingPair }) :
                  Type u))))).toIntAlgHom
⊢ Hom.hom { hom' := m } =
    Hom.hom
      (ofHom
        (AlgHom.toRingHom
          (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
            (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u) →ₐ[ℤ]
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))))

Tactic:
apply RingHom.toIntAlgHom_injective

Premises used: RingHom.toIntAlgHom_injective
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : BinaryCofan A B
m : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →+* (↑s.pt : Type u)
hm : ∀ (j : Discrete WalkingPair), (A.coproductCocone B).ι.app j ≫ { hom' := m } = s.ι.app j
a : (↑A : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((AlgHom.comp (B := (↑A : Type u) ⊗[ℤ] (↑B : Type u))
            (RingHom.toIntAlgHom (Hom.hom { hom' := m }) : (↑(A.coproductCocone B).pt : Type u) →ₐ[ℤ] (↑s.pt : Type u))
            Algebra.TensorProduct.includeLeft :
          (a : (↑A : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))
    (((((Equiv.symm Algebra.TensorProduct.liftEquiv :
                    ((↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) ≃
                      { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                          Commute (S := (↑s.pt : Type u))
                            ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
                            ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y : (↑s.pt : Type u)) }) :
                  (a : (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) →
                    { fg : ((↑A : Type u) →ₐ[ℤ] (↑s.pt : Type u)) × ((↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u)) //
                      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                        Commute ((fg.1 : (a : (↑A : Type u)) → (↑s.pt : Type u)) x)
                          ((fg.2 : (a : (↑B : Type u)) → (↑s.pt : Type u)) y) })
                (Hom.hom
                    (ofHom
                      (AlgHom.toRingHom
                        (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom ⋯ :
                          (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ⊗[ℤ]
                              (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) :
                                Type u) →ₐ[ℤ]
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) s.pt)
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                              Type u))))).toIntAlgHom).1.1 :
          (a : (↑A : Type u)) → (↑s.pt : Type u))
        a :
      (↑s.pt : Type u))

Tactic:
simp [map_one, mul_one, ← hm (Discrete.mk WalkingPair.left)]

Premises used: CategoryTheory.Discrete.mk, map_one, mul_one, CategoryTheory.Limits.WalkingPair.left