awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommRingCat
x x_1 : J
f : x ⟶ x_1
x_2 : (↑(F.obj x) : Type (max u v))
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (RingCat.Hom.hom
                  ((RingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                              fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              RingCat.carrier))).ι.app
                    x_1))) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (ofHom
                (RingCat.Hom.hom
                  ((RingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ CommRingCat (FC := fun (R S : CommRingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) RingCat (FD :=
                              fun (R S : RingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              RingCat.carrier))).ι.app
                    x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit.{v, u} F)) f) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))

Tactic:
simpa using (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _

Premises used: CategoryTheory.NatTrans.naturality_apply, CommRingCat, CategoryTheory.Limits.Types.TypeMax.colimitCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.Cocone.ι, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommRingCat
⊢ PreservesFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ CommRingCat RingCat) (forget RingCat.{u})

Premises used: CommRingCat, CategoryTheory.Functor.comp, RingCat, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
inl : IsEmpty J → Nontrivial.{v} (↑c.pt : Type v)
inr : Nonempty J → Nontrivial.{v} (↑c.pt : Type v)
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
cases isEmpty_or_nonempty J

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h : IsEmpty J
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
((isColimitEquivIsInitialOfIsEmpty _ _ hc).to (.of (ULift ℤ))).hom.domain_nontrivial

Premises used: CommRingCat.Hom.hom, ULift, Int, CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty, CategoryTheory.Limits.IsInitial.to, CommRingCat.of, RingHom.domain_nontrivial, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h : IsEmpty J
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
exact ((isColimitEquivIsInitialOfIsEmpty _ _ hc).to (.of (ULift ℤ))).hom.domain_nontrivial

Premises used: CommRingCat.Hom.hom, ULift, Int, CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty, CategoryTheory.Limits.IsInitial.to, CommRingCat.of, RingHom.domain_nontrivial, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h : Nonempty J
inr : ∀ (i : J), Nontrivial.{v} (↑c.pt : Type v)
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
have i := ‹Nonempty J›.some
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h : Nonempty J
i : J
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Nontrivial.mk, CategoryTheory.Limits.Cocone.ι, Exists.intro, OfNat.ofNat, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h : Nonempty J
i : J
inr :
  ∀
    (h :
      Eq (α := (↑c.pt : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                (c.ι.app i) :
              (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
            0 :
          (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
                (c.ι.app i) :
              (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
            1 :
          (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))),
    False
⊢ Nontrivial.{v} (↑c.pt : Type v)

Tactic:
refine ⟨c.ι.app i 0, c.ι.app i 1, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h_1 : Nonempty J
i : J
h :
  Eq (α := (↑c.pt : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        0 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        1 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
⊢ IsFiltered J

Tactic:
have : IsFiltered J := ⟨⟩
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h_1 : Nonempty J
i : J
h :
  Eq (α := (↑c.pt : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        0 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        1 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
this : IsFiltered J
k : J
f : i ⟶ k
e :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      ((F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
              carrier)).obj
        k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  carrier)).map
            f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
          (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
      0)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  carrier)).map
            f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
          (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
      1)
⊢ False

Tactic:
zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)

Premises used: CommRingCat.Hom.hom, RingHom.map_one, zero_ne_one, CategoryTheory.Functor.map, RingHom.map_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CommRingCat
inst_1 : IsFilteredOrEmpty J
inst_2 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
c : Cocone F
hc : IsColimit c
h_1 : Nonempty J
i : J
h :
  Eq (α := (↑c.pt : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        0 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC := carrier)
            (c.ι.app i) :
          (a : (↑(F.obj i) : Type v)) → (↑(((Functor.const J).obj c.pt).obj i) : Type v))
        1 :
      (↑(Functor.obj (Functor.obj (Functor.const J) c.pt) i) : Type v))
this : IsFiltered J
k : J
f : i ⟶ k
e :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      ((F ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
              carrier)).obj
        k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  carrier)).map
            f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
          (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
      0)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CC :=
                  carrier)).map
            f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj i)) →
          (fun (X : Type v) ↦ X) ((F ⋙ forget CommRingCat).obj k))
      1)
⊢ False

Tactic:
exact zero_ne_one (((F.map f).hom.map_zero.symm.trans e).trans (F.map f).hom.map_one)

Premises used: CommRingCat.Hom.hom, RingHom.map_one, zero_ne_one, CategoryTheory.Functor.map, RingHom.map_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F_1 : J ⥤ CommRingCat
F : J ⥤ CommRingCat
inst_2 : IsFilteredOrEmpty J
inst_3 : HasColimit F
inst_4 : ∀ (i : J), Nontrivial.{v} (↑(F.obj i) : Type v)
⊢ Nontrivial.{v} (↑(Limits.colimit F) : Type v)

Tactic:
FilteredColimits.nontrivial (getColimitCocone F).2

Premises used: CommRingCat.FilteredColimits.nontrivial, CategoryTheory.Limits.ColimitCocone.isColimit, CategoryTheory.Limits.getColimitCocone
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
hf : (CommRingCat.Hom.hom f).FinitePresentation
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
have :
  ∀
    (hc' :
      IsColimit (F :=
        F ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (Functor.mapCocone
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          c)),
    ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i

Tactic:
have hc' := isColimitOfPreserves (forget _) hc
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
hf : (CommRingCat.Hom.hom f).FinitePresentation
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
obtain :
  ∀ (n : ℕ)
    (hn :
      ∃ (f_1 : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
        Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
            (⇑f_1 : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
          Ideal.FG (ker f_1.toRingHom)),
    ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i

Tactic:
obtain ⟨n, hn⟩ := hf
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
hn :
  ∃ (f_1 : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f_1 : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f_1.toRingHom)
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
obtain :
  ∀ (π : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u))
    (h₁ :
      Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑π : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)))
    (h₂ : Ideal.FG (ker π.toRingHom)),
    ∃ (π : P ⟶ S),
      iP ≫ π = f ∧
        Function.Surjective (α := (↑P : Type u)) (β := (↑S : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) π) :
              (a : (↑P : Type u)) → (↑S : Type u)) ∧
          Ideal.FG (ker (CommRingCat.Hom.hom π))
⊢ ∃ (π : P ⟶ S),
    iP ≫ π = f ∧
      Function.Surjective (α := (↑P : Type u)) (β := (↑S : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) π) :
            (a : (↑P : Type u)) → (↑S : Type u)) ∧
        Ideal.FG (ker (CommRingCat.Hom.hom π))

Tactic:
obtain ⟨π, h₁, h₂⟩ := hn
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)
h₁ :
  Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
    (⇑π : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u))
h₂ : Ideal.FG (ker π.toRingHom)
hf :
  CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u))) =
    CommRingCat.Hom.hom f
⊢ iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u)) = f

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)
h₁ :
  Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
    (⇑π : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u))
h₂ : Ideal.FG (ker π.toRingHom)
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u))) =
    CommRingCat.Hom.hom f

Tactic:
π.comp_algebraMap

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)
h₁ :
  Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
    (⇑π : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u))
h₂ : Ideal.FG (ker π.toRingHom)
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u))) =
    CommRingCat.Hom.hom f

Tactic:
exact π.comp_algebraMap

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J CommRingCat
α : Functor.obj (Functor.const J) R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst_2 :
  PreservesColimit F
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' :
  IsColimit (F :=
    F ⋙
      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
    (Functor.mapCocone
      (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier))
      c)
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)
h₁ :
  Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
    (⇑π : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u))
h₂ : Ideal.FG (ker π.toRingHom)
⊢ ∃ (π : P ⟶ S),
    iP ≫ π = f ∧
      Function.Surjective (α := (↑P : Type u)) (β := (↑S : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) π) :
            (a : (↑P : Type u)) → (↑S : Type u)) ∧
        Ideal.FG (ker (CommRingCat.Hom.hom π))

Tactic:
exact ⟨CommRingCat.ofHom π, by ext1; exact π.comp_algebraMap, h₁, h₂⟩