awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
j : WalkingPair
⊢ 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 })
have 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 sorry :
          (↑(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: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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 })
⊢ 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 })
have 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 sorry :
          (↑(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: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
⊢ 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 })
have 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 sorry :
                    (↑(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: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
s : BinaryCofan A B
x : Discrete WalkingPair
⊢ 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 })
have 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 sorry :
                    (↑(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: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ { 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)))
have hf : Hom.hom { hom' := m } =
  Hom.hom
    (ofHom
      (AlgHom.toRingHom
        (Algebra.TensorProduct.lift (Hom.hom s.inl).toIntAlgHom (Hom.hom s.inr).toIntAlgHom sorry :
          (↑(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
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ 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))))
have 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 sorry :
            (↑(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
Tactic: apply RingHom.toIntAlgHom_injective
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
⊢ HasStrictTerminalObjects CommRingCat
have apply : ∀ (A : CommRingCat.{u}) (f : of PUnit.{u + 1} ⟶ A), IsIso f
Tactic: apply hasStrictTerminalObjects_of_terminal_is_strict (CommRingCat.of PUnit)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ IsIso f
have refine_1 : f ≫ ofHom { toMonoidHom := 1, map_zero' := sorry, map_add' := sorry } = 𝟙 (of PUnit.{u + 1})
Tactic: refine ⟨ofHom ⟨1, rfl, by simp⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
refine_1 : f ≫ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } = 𝟙 (of PUnit.{u + 1})
⊢ IsIso f
have refine_2 : ofHom { toMonoidHom := 1, map_zero' := sorry, map_add' := sorry } ≫ f = 𝟙 X
Tactic: refine ⟨ofHom ⟨1, rfl, by simp⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X
have refine_2 : ∀ (x : (↑X : Type u)),
  Eq (α := (↑X : Type u))
    ((Hom.hom (ofHom { toMonoidHom := 1, map_zero' := sorry, map_add' := sorry } ≫ 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: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
⊢ Eq.{u + 1} (α := (↑X : Type u)) 0 1
have 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))
Tactic: rw [← f.hom.map_one, ← f.hom.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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))
⊢ Eq.{u + 1} (α := (↑X : Type u)) 0 1
have 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))
Tactic: rw [← f.hom.map_one, ← f.hom.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
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))
have e : Eq.{u + 1} (α := (↑X : Type u)) 0 1
Tactic: have e : (0 : X) = 1 := by
      rw [← f.hom.map_one, ← f.hom.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : Eq.{u + 1} (α := (↑X : Type u)) 0 1
⊢ 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))
have e₁ : 0 * x = 1 * x
Tactic: replace e : 0 * x = 1 * x := congr_arg (· * x) e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : (↑X : Type u)
e : 0 * x = 1 * 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))
have e₁ : (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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R : CommRingCat
x : of (ULift.{u, 0} ℤ) ⟶ R
⊢ x = default
have hf : Hom.hom x = Hom.hom default
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
R : CommRingCat
x : of (ULift.{u, 0} ℤ) ⟶ R
⊢ Hom.hom x = Hom.hom default
have 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)))
Tactic: rw [← RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom)
        (hf := ULift.ringEquiv.symm.surjective)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
c : Cone (pair A B)
j : Discrete WalkingPair
x : (↑c.pt : Type u)
⊢ Eq (α := (↑(Functor.obj (pair A B) j) : Type u))
    (((Hom.hom
              (ofHom
                  (RingHom.prod (Hom.hom (c.π.app { as := WalkingPair.left }))
                    (Hom.hom (c.π.app { as := WalkingPair.right }))) ≫
                (A.prodFan B).π.app j) :
            (↑c.pt : Type u) →+* (↑(Functor.obj (pair A B) j) : Type u)) :
          (a : (↑c.pt : Type u)) → (↑((pair A B).obj j) : Type u))
        x :
      (↑(Functor.obj (pair A B) j) : Type u))
    ((Hom.hom (c.π.app j) : (a : (↑c.pt : Type u)) → (↑((pair A B).obj j) : Type u)) x :
      (↑(Functor.obj (pair A B) j) : Type u))
have hf : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
c : Cone (pair A B)
x : (↑c.pt : 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))
have 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))
Tactic: simp only [pair_obj_left, prodFan_pt, BinaryFan.π_app_left, BinaryFan.π_app_right]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
              (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))
have 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))
Tactic: simp only [pair_obj_left, prodFan_pt, BinaryFan.π_app_left, BinaryFan.π_app_right]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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
⊢ m =
    ofHom (RingHom.prod (Hom.hom (s.π.app { as := WalkingPair.left })) (Hom.hom (s.π.app { as := WalkingPair.right })))
have 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))
Tactic: ext x