awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
F : WalkingParallelPair ⥤ CommRingCat
this :
  Eq (α := limit F ⟶ F.obj WalkingParallelPair.zero)
    (CategoryStruct.comp (Y :=
        limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
        (limMap (diagramIsoParallelPair F).hom)
        (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
          WalkingParallelPair.zero) ≫
      inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero))
    (limit.π F WalkingParallelPair.zero)
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom (limit.π F WalkingParallelPair.zero))
have rw : IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
  (↑(limit F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
  (Hom.hom
    (CategoryStruct.comp (Y :=
        limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
        (limMap (diagramIsoParallelPair F).hom)
        (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
          WalkingParallelPair.zero) ≫
      inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj (op one)) : Type u)) (Hom.hom (limit.π F (op one)))
have this : CategoryStruct.comp (Y := limit (walkingParallelPairOpEquiv.functor ⋙ F))
    (Iso.inv
      (limit.isoLimitCone
        { cone := Cone.whisker walkingParallelPairOpEquiv.functor (limit.cone F),
          isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
          LimitCone (walkingParallelPairOpEquiv.functor ⋙ F) }))
    (limit.π (walkingParallelPairOpEquiv.functor ⋙ F) zero) =
  { cone := Cone.whisker walkingParallelPairOpEquiv.functor (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv }.cone.π.app
    zero
Tactic: have := limit.isoLimitCone_inv_π
    ⟨_, IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv⟩
        WalkingParallelPair.zero
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this :
  CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero) =
    limit.π F (op one)
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj (op one)) : Type u)) (Hom.hom (limit.π F (op one)))
have rw : IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u))
  (Hom.hom
    (CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero)))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this :
  CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
      (Iso.inv
        (limit.isoLimitCone
          { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
            isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
            LimitCone (walkingParallelPairOp ⋙ F) }))
      (limit.π (walkingParallelPairOp ⋙ F) zero) =
    limit.π F (op one)
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj (op one)) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y := limit (walkingParallelPairOp ⋙ F))
        (Iso.inv
          (limit.isoLimitCone
            { cone := Cone.whisker walkingParallelPairOp (limit.cone F),
              isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) walkingParallelPairOpEquiv :
              LimitCone (walkingParallelPairOp ⋙ F) }))
        (limit.π (walkingParallelPairOp ⋙ F) zero)))
have this₁ : IsLocalHom (R := (↑(limit (walkingParallelPairOp ⋙ F)) : Type u)) (S :=
  (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u)) (F :=
  (↑(limit (walkingParallelPairOp ⋙ F)) : Type u) →+* (↑((walkingParallelPairOp ⋙ F).obj zero) : Type u))
  (Hom.hom (limit.π (walkingParallelPairOp ⋙ F) zero))
Tactic: have : IsLocalHom (limit.π (walkingParallelPairOp ⋙ F) zero).hom := by infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ Eq (α :=
    of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))) ⟶
      C)
    (ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) ≫
      f)
    (ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) ≫
      g)
have hf : ∀ (x : (↑A : Type u) × (↑B : Type u))
  (e :
    Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
      (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
      x),
  Eq (α := (↑C : Type u))
    ((Hom.hom
            (ofHom
                (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
                  (Subring.subtype
                    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) ≫
              f) :
          (a :
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u)) →
            (↑C : Type u))
        (Subtype.mk (p := fun (x : (↑A : Type u) × (↑B : Type u)) ↦
          Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            x)
          x e) :
      (↑C : Type u))
    ((Hom.hom
            (ofHom
                (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
                  (Subring.subtype
                    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) ≫
              g) :
          (a :
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u)) →
            (↑C : Type u))
        (Subtype.mk (p := fun (x : (↑A : Type u) × (↑B : Type u)) ↦
          Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            x)
          x e) :
      (↑C : Type u))
Tactic: ext ⟨x, e⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ IsLimit (pullbackCone f g)
have lift : (s : PullbackCone f g) →
  s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
Tactic: fapply PullbackCone.IsLimit.mk
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
lift :
  (s : PullbackCone f g) →
    s.pt ⟶
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
⊢ IsLimit (pullbackCone f g)
have fac_left : ∀ (s : PullbackCone f g),
  CategoryStruct.comp (Y :=
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
      (ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
          sorry))
      (ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
    s.fst
Tactic: fapply PullbackCone.IsLimit.mk
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
lift :
  (s : PullbackCone f g) →
    s.pt ⟶
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
fac_left :
  ∀ (s : PullbackCone f g),
    CategoryStruct.comp (Y :=
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
        (ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            ⋯))
        (ofHom
          (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
      s.fst
⊢ IsLimit (pullbackCone f g)
have fac_right : ∀ (s : PullbackCone f g),
  CategoryStruct.comp (Y :=
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
      (ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
          sorry))
      (ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
    s.snd
Tactic: fapply PullbackCone.IsLimit.mk
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
lift :
  (s : PullbackCone f g) →
    s.pt ⟶
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
fac_left :
  ∀ (s : PullbackCone f g),
    CategoryStruct.comp (Y :=
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
        (ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            ⋯))
        (ofHom
          (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
      s.fst
fac_right :
  ∀ (s : PullbackCone f g),
    CategoryStruct.comp (Y :=
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
        (ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            ⋯))
        (ofHom
          (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
      s.snd
⊢ IsLimit (pullbackCone f g)
have uniq : ∀ (s : PullbackCone f g)
  (m :
    s.pt ⟶
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))),
  m ≫
        ofHom
          (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
      s.fst →
    m ≫
          ofHom
            (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
              (Subring.subtype
                (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                  ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
        s.snd →
      m =
        ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            sorry)
Tactic: fapply PullbackCone.IsLimit.mk
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
have lift : ∀ (x : (↑s.pt : Type u)),
  Membership.mem (α := (↑A : Type u) × (↑B : Type u)) (γ := Subring ((↑A : Type u) × (↑B : Type u)))
    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
    (((Hom.hom s.fst).prod (Hom.hom s.snd) : (a : (↑s.pt : Type u)) → (↑A : Type u) × (↑B : Type u)) x :
      (↑A : Type u) × (↑B : Type u))
Tactic: refine ofHom ((s.fst.hom.prod s.snd.hom).codRestrict _ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ CategoryStruct.comp (Y :=
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
      (ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
          ⋯))
      (ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
    s.fst
have fac_left : ∀ (x : (↑s.pt : Type u)),
  Eq (α := (↑A : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y :=
              of
                ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
              (ofHom
                (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
                  sorry))
              (ofHom
                (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
                  (Subring.subtype
                    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))))) :
          (a : (↑s.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ CategoryStruct.comp (Y :=
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
      (ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
          ⋯))
      (ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
    s.snd
have fac_right : ∀ (x : (↑s.pt : Type u)),
  Eq (α := (↑B : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y :=
              of
                ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
              (ofHom
                (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
                  sorry))
              (ofHom
                (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
                  (Subring.subtype
                    (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                      ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))))) :
          (a : (↑s.pt : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x : (↑B : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m :
  s.pt ⟶
    of
      ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
e₁ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.fst
e₂ :
  m ≫
      ofHom
        (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
          (Subring.subtype
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
    s.snd
⊢ m =
    ofHom
      (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
        (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
        ⋯)
have uniq : ∀ (x : (↑s.pt : Type u)),
  Eq.{u + 1} (α := (↑A : Type u) × (↑B : Type u))
    (↑((Hom.hom m :
            (a : (↑s.pt : Type u)) →
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u))
          x) :
      (↑A : Type u) × (↑B : Type u))
    (↑((Hom.hom
              (ofHom
                (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
                  sorry)) :
            (a : (↑s.pt : Type u)) →
              (↑(of
                    ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                        ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                Type u))
          x) :
      (↑A : Type u) × (↑B : Type u))
Tactic: refine hom_ext <| RingHom.ext fun (x : s.pt) => Subtype.ext ?_