awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPairᵒᵖ ⥤ CommRingCat
this_1 :
  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)
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))
⊢ 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:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
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:
simpa [CommRingCat.ofHom] using e

Premises used: CommRingCat.ofHom
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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))
⊢ 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:
refine ofHom ((s.fst.hom.prod s.snd.hom).codRestrict _ ?_)

Premises used: CommRingCat.ofHom
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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:
congr_arg (fun f : s.pt →+* C => f x) (congrArg Hom.hom s.condition)

Premises used: CommRingCat.Hom.hom, CategoryTheory.Limits.PullbackCone.condition, congrArg, Set.Mem, setOf, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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:
exact congr_arg (fun f : s.pt →+* C => f x) (congrArg Hom.hom s.condition)

Premises used: CommRingCat.Hom.hom, CategoryTheory.Limits.PullbackCone.condition, congrArg, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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))))
                    ⋯))
                (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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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))))
                  ⋯))
              (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:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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))))
                    ⋯))
                (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))
⊢ 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

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
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))))
                  ⋯))
              (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:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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))))
        ⋯)

Tactic:
hom_ext <| RingHom.ext fun (x : s.pt) => Subtype.ext ?_

Premises used: CommRingCat.hom_ext, RingHom.ext, Subtype.ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
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))))
                    ⋯)) :
              (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))
⊢ 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))))
        ⋯)

Tactic:
refine hom_ext <| RingHom.ext fun (x : s.pt) => Subtype.ext ?_

Premises used: CommRingCat.hom_ext, RingHom.ext, Subtype.ext
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
x : (↑s.pt : Type u)
uniq :
  Eq (α := (↑A : Type u) × (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) 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)) :
      (↑A : Type u) × (↑B : Type u))
    (((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x,
        (Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x) :
      (↑A : Type u) × (↑B : 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))))
                  ⋯)) :
            (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:
change (m x).1 = (_, _)

Premises used: CategoryTheory.ConcreteCategory.hom, Prod.mk, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
x : (↑s.pt : Type u)
⊢ Eq (α := (↑A : Type u))
    ((Hom.hom
            (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))))))) :
          (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:
have eq1 := (congr_arg (fun f : s.pt →+* A => f x) (congrArg Hom.hom e₁) :)
-- Module: Mathlib.Algebra.Category.Ring.Constructions
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
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑A : Type u))
    ((Hom.hom
            (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))))))) :
          (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))
⊢ Eq (α := (↑B : Type u))
    ((Hom.hom
            (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))))))) :
          (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:
have eq2 := (congr_arg (fun f : s.pt →+* B => f x) (congrArg Hom.hom e₂) :)
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
simp_rw : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
⊢ Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

Tactic:
simp_rw [Algebra.isEpi_iff_forall_one_tmul_eq, eq_comm]

Premises used: eq_comm, Algebra.isEpi_iff_forall_one_tmul_eq
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
mp : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) → ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)
mpr : (∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)) → Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
⊢ Epi (X := of R) (Y := of S) (ofHom (algebraMap R S)) ↔ ∀ (a : S), Eq (α := S ⊗[R] S) (a ⊗ₜ[R] 1) (1 ⊗ₜ[R] a)

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Epi
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
H : Epi (X := of R) (Y := of S) (ofHom (algebraMap R S))
hf :
  ∀ (r : (↑(of R) : Type u)),
    Eq (α := (↑(of (S ⊗[R] S)) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
                (ofHom Algebra.TensorProduct.includeLeftRingHom)) :
            (a : (↑(of R) : Type u)) → (↑(of (S ⊗[R] S)) : Type u))
          r :
        (↑(of (S ⊗[R] S)) : Type u))
      ((Hom.hom
              (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
                (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight))) :
            (a : (↑(of R) : Type u)) → (↑(of (S ⊗[R] S)) : Type u))
          r :
        (↑(of (S ⊗[R] S)) : Type u))
⊢ Eq (α := of R ⟶ of (S ⊗[R] S))
    (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S)) (ofHom Algebra.TensorProduct.includeLeftRingHom))
    (CategoryStruct.comp (Y := of S) (ofHom (algebraMap R S))
      (ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight)))

Tactic:
ext r