awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b : (↑B : Type u)
⊢ Eq (α := (↑s.pt : Type u))
    ((AlgHom.comp (B := (↑A : Type u) ⊗[ℤ] (↑B : Type u))
            (AlgHom.restrictScalars ℤ (S := ℤ) (RingHom.toIntAlgHom (Hom.hom { hom' := m })) :
              (↑A : Type u) ⊗[ℤ] (↑B : Type u) →ₐ[ℤ] (↑s.pt : Type u))
            (Algebra.TensorProduct.includeRight : (↑B : Type u) →ₐ[ℤ] (↑A : Type u) ⊗[ℤ] (↑B : Type u)) :
          (a : (↑B : Type u)) → (↑s.pt : Type u))
        b :
      (↑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.2 :
          (a : (↑B : Type u)) → (↑s.pt : Type u))
        b :
      (↑s.pt : Type u))

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

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, map_one
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
⊢ ∀ (x y : (↑X : Type u)),
    OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) (x + y) =
      HAdd.hAdd (α := PUnit.{u + 1}) (OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) x)
        (OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) y)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : X ⟶ of PUnit.{u + 1}
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
apply : ∀ (A : CommRingCat.{u}) (f : of PUnit.{u + 1} ⟶ A), IsIso f
⊢ HasStrictTerminalObjects CommRingCat

Tactic:
apply hasStrictTerminalObjects_of_terminal_is_strict (CommRingCat.of PUnit)

Premises used: PUnit, CommRingCat.of, CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ∀ (x y : (↑X : Type u)),
    OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) (x + y) =
      HAdd.hAdd (α := PUnit.{u + 1}) (OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) x)
        (OneHom.toFun (↑1 : OneHom (↑X : Type u) PUnit.{u + 1}) y)

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
refine_1 : f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})
refine_2 : ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X
⊢ IsIso f

Tactic:
refine ⟨ofHom ⟨1, rfl, by simp⟩, ?_, ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
refine_2 :
  ∀ (x : (↑X : Type u)),
    Eq (α := (↑X : Type u))
      ((Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f) : (a : (↑X : Type u)) → (↑X : Type u))
          x :
        (↑X : Type u))
      ((Hom.hom (𝟙 X) : (a : (↑X : Type u)) → (↑X : Type u)) x : (↑X : Type u))
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
rw :
  Eq (α := (↑X : Type u)) (0 : (↑X : Type u))
    ((Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 1 : (↑X : Type u))
rw₁ rw₂ :
  Eq (α := (↑X : Type u)) ((Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 0 : (↑X : Type u))
    ((Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 1 : (↑X : Type u))
⊢ Eq.{u + 1} (α := (↑X : Type u)) 0 1

Tactic:
rw [← f.hom.map_one, ← f.hom.map_zero]

Premises used: CommRingCat.Hom.hom, RingHom.map_one, RingHom.map_zero
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
⊢ Eq.{u + 1} (α := (↑X : Type u)) 0 1

Tactic:
have e : (0 : X) = 1 := by
      rw [← f.hom.map_one, ← f.hom.map_zero]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : Eq.{u + 1} (α := (↑X : Type u)) 0 1
⊢ 0 * x = 1 * x

Tactic:
replace e : 0 * x = 1 * x := congr_arg (· * x) e
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : 0 * x = 1 * x
⊢ (Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 0 = x

Tactic:
rw [one_mul, zero_mul, ← f.hom.map_zero] at e

Premises used: CommRingCat.Hom.hom, MulZeroClass.zero_mul, RingHom.map_zero, one_mul
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : (Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 0 = x
⊢ Eq (α := (↑X : Type u))
    ((Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f) : (a : (↑X : Type u)) → (↑X : Type u)) x :
      (↑X : Type u))
    ((Hom.hom (𝟙 X) : (a : (↑X : Type u)) → (↑X : Type u)) x : (↑X : Type u))

Tactic:
e
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : (Hom.hom f : (a : (↑(of PUnit.{u + 1}) : Type u)) → (↑X : Type u)) 0 = x
⊢ Eq (α := (↑X : Type u))
    ((Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f) : (a : (↑X : Type u)) → (↑X : Type u)) x :
      (↑X : Type u))
    ((Hom.hom (𝟙 X) : (a : (↑X : Type u)) → (↑X : Type u)) x : (↑X : Type u))

Tactic:
exact e
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
X : CommRingCat
hX : IsTerminal X
⊢ Subsingleton PUnit.{u_1 + 1}

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R : CommRingCat
x : of (ULift.{u, 0} ℤ) ⟶ R
hf : Hom.hom x = Hom.hom default
⊢ x = default

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R : CommRingCat
x : of (ULift.{u, 0} ℤ) ⟶ R
hf :
  Eq (α := ℤ →+* (↑R : Type u)) ((Hom.hom x).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv)))
    (@RingHom.comp _ (ULift.{u, 0} ℤ) _ _ (ULift.nonAssocSemiring : NonAssocSemiring (ULift.{u, 0} ℤ)) _
      (Hom.hom default : (↑(of (ULift.{u, 0} ℤ)) : Type u) →+* (↑R : Type u))
      (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv)))
⊢ Hom.hom x = Hom.hom default

Tactic:
rw [← RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom)
        (hf := ULift.ringEquiv.symm.surjective)]
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
R : CommRingCat
x : of (ULift.{u, 0} ℤ) ⟶ R
⊢ Eq (α := ℤ →+* (↑R : Type u)) ((Hom.hom x).comp (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv)))
    (@RingHom.comp _ (ULift.{u, 0} ℤ) _ _ (ULift.nonAssocSemiring : NonAssocSemiring (ULift.{u, 0} ℤ)) _
      (Hom.hom default : (↑(of (ULift.{u, 0} ℤ)) : Type u) →+* (↑R : Type u))
      (RingEquiv.toRingHom (RingEquiv.symm ULift.ringEquiv)))

Tactic:
apply RingHom.ext_int

Premises used: RingHom.ext_int
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
c : Cone (pair A B)
x : (↑c.pt : Type u)
hf :
  Eq (α := (↑A : Type u))
    ((Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).fst) :
          (a : (↑c.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom (BinaryFan.fst c) : (a : (↑c.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
⊢ Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    (((Hom.hom
              (CategoryStruct.comp (Y := (A.prodFan B).pt)
                (ofHom
                    (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                      (Hom.hom (c.π.app { as := WalkingPair.right }))) :
                  of (↑c.1 : Type u) ⟶ of ((↑A : Type u) × (↑B : Type u)))
                ((A.prodFan B).π.app { as := WalkingPair.left } :
                  Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (A.prodFan B).pt)
                      { as := WalkingPair.left : Discrete WalkingPair } ⟶
                    Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair })) :
            (↑c.pt : Type u) →+*
              (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((Hom.hom (c.π.app { as := WalkingPair.left }) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
simp only [pair_obj_left, prodFan_pt, BinaryFan.π_app_left, BinaryFan.π_app_right]

Premises used: CategoryTheory.Limits.BinaryFan.π_app_right, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Limits.BinaryFan.π_app_left, CommRingCat.prodFan_pt
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
c : Cone (pair A B)
x : (↑c.pt : Type u)
hf :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).snd) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((Hom.hom (BinaryFan.snd c) : (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    (((Hom.hom
              (CategoryStruct.comp (Y := (A.prodFan B).pt)
                (ofHom
                    (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                      (Hom.hom (c.π.app { as := WalkingPair.right }))) :
                  of (↑c.1 : Type u) ⟶ of ((↑A : Type u) × (↑B : Type u)))
                ((A.prodFan B).π.app { as := WalkingPair.right } :
                  Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (A.prodFan B).pt)
                      { as := WalkingPair.right : Discrete WalkingPair } ⟶
                    Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :
            (↑c.pt : Type u) →+*
              (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((Hom.hom (c.π.app { as := WalkingPair.right }) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))

Tactic:
simp only [pair_obj_left, prodFan_pt, BinaryFan.π_app_left, BinaryFan.π_app_right]

Premises used: CategoryTheory.Limits.BinaryFan.π_app_right, CategoryTheory.Limits.pair_obj_left, CategoryTheory.Limits.BinaryFan.π_app_left, CommRingCat.prodFan_pt
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
c : Cone (pair A B)
x : (↑c.pt : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).fst) :
          (a : (↑c.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom (BinaryFan.fst c) : (a : (↑c.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
c : Cone (pair A B)
x : (↑c.pt : Type u)
⊢ Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((Hom.hom (ofHom ((Hom.hom (BinaryFan.fst c)).prod (Hom.hom (BinaryFan.snd c))) ≫ (A.prodFan B).snd) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((Hom.hom (BinaryFan.snd c) : (a : (↑c.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u)) x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
hf :
  ∀ (x : (↑s.pt : Type u)),
    Eq (α := (↑(A.prodFan B).pt : Type u))
      ((Hom.hom m : (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u)) x : (↑(A.prodFan B).pt : Type u))
      (((Hom.hom
                (ofHom
                  (RingHom.prod (Hom.hom (s.π.app { as := WalkingPair.left }))
                    (Hom.hom (s.π.app { as := WalkingPair.right })))) :
              (↑s.pt : Type u) →+* (↑(A.prodFan B).pt : Type u)) :
            (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
          x :
        (↑(A.prodFan B).pt : Type u))
⊢ m =
    ofHom (RingHom.prod (Hom.hom (s.π.app { as := WalkingPair.left })) (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
hf :
  Eq (α := (↑(A.prodFan B).pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.fst s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.snd s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
          x) :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(A.prodFan B).pt : Type u))
    ((Hom.hom m : (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u)) x : (↑(A.prodFan B).pt : Type u))
    (((Hom.hom
              (ofHom
                (RingHom.prod (Hom.hom (s.π.app { as := WalkingPair.left }))
                  (Hom.hom (s.π.app { as := WalkingPair.right })))) :
            (↑s.pt : Type u) →+* (↑(A.prodFan B).pt : Type u)) :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))

Tactic:
change m x = (BinaryFan.fst s x, BinaryFan.snd s x)

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.ConcreteCategory.hom, Prod.mk, CategoryTheory.Limits.BinaryFan.snd, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
⊢ Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).fst) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.fst s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
have eq1 : (m ≫ (A.prodFan B).fst) x = (BinaryFan.fst s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.left⟩) x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).fst) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.fst s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).snd) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.snd s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))

Tactic:
have eq2 : (m ≫ (A.prodFan B).snd) x = (BinaryFan.snd s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.right⟩) x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).fst) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.fst s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
eq2 :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).snd) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.snd s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(A.prodFan B).pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (m ≫ (A.prodFan B).fst) :
            (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (m ≫ (A.prodFan B).snd) :
            (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
          x) :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))

Tactic:
simp [prodFan]

Premises used: CommRingCat.prodFan
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
ι : Type u
R : ι → CommRingCat
s : Cone (Discrete.functor R)
i : Discrete ι
⊢ ofHom (Pi.ringHom (f := fun (i : ι) ↦ (↑(R i) : Type u)) fun (i : ι) ↦ Hom.hom (s.π.app { as := i })) ≫
      (piFan R).π.app i =
    s.π.app i

Tactic:
rfl