awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have 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
Tactic: obtain ⟨n, hn⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
⊢ ∃ (π : 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 π))
have 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 π))
Tactic: obtain ⟨π, h₁, h₂⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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)
⊢ iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u)) = f
have hf : CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom (↑π : MvPolynomial (Fin n) (↑R : Type u) →+* (↑S : Type u))) =
  CommRingCat.Hom.hom f
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have obtain : ∀ (π : P ⟶ S) (hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i)
  (hn :
    ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
      Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
          (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
        Ideal.FG (ker f.toRingHom))
  (hπ :
    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)))
  (s : Finset (↑P : Type u))
  (hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))),
  ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
Tactic: obtain ⟨π, rfl, hπ, s, hs⟩ :
      ∃ π : P ⟶ S, iP ≫ π = f ∧ Function.Surjective π ∧ (RingHom.ker π.hom).FG := by
    obtain ⟨π, h₁, h₂⟩ := hn
    exact ⟨CommRingCat.ofHom π, by ext1; exact π.comp_algebraMap, h₁, h₂⟩
Cleared hypotheses: f, hg, this, hn
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
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
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)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  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))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have obtain : ∀ (i : J) (g' : P ⟶ F.obj i) (hg' : π ≫ g = g' ≫ c.ι.app i) (hg'' : iP ≫ g' = α.app i),
  ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
Tactic: obtain ⟨i, g', hg', hg''⟩ : ∃ (i : J) (g' : P ⟶ F.obj i),
      π ≫ g = g' ≫ c.ι.app i ∧ iP ≫ g' = α.app i := by
    choose j x h using fun i ↦ Types.jointly_surjective_of_isColimit hc' ((π ≫ g) (.X i))
    obtain ⟨i, ⟨hi⟩⟩ : ∃ i, Nonempty (∀ a, (j a ⟶ i)) := by
      have : ∃ i, ∀ a, Nonempty (j a ⟶ i) := by
        simpa using IsFiltered.sup_objs_exists (Finset.univ.image j)
      simpa [← exists_true_iff_nonempty, Classical.skolem, -exists_const_iff] using this
    refine ⟨i, CommRingCat.ofHom (MvPolynomial.eval₂Hom
      (α.app i).hom (F.map (hi _) <| x ·)), ?_, ?_⟩
    · ext1
      apply MvPolynomial.ringHom_ext
      · simpa using fun x ↦ congr($(hg i).hom x)
      · intro i
        simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
          Functor.const_obj_obj, CommRingCat.hom_ofHom, MvPolynomial.coe_eval₂Hom,
          MvPolynomial.eval₂_X]
        exact (congr($(c.w (hi i)).hom (x i)).trans (h i)).symm
    · ext x
      simp [P, iP]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (hypothesis)
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
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
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)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  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))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have this₁ : ∀ (r : ↥s),
  ∃ (i' : J) (hi' : i ⟶ i'),
    Eq (α := (↑(F.obj i') : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map hi') :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj i') : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj i') : Type u))
      (0 : (↑(F.obj i') : Type u))
Tactic: have : ∀ r : s, ∃ (i' : J) (hi' : i ⟶ i'), F.map hi' (g' r) = 0 := by
    intro r
    have := Types.FilteredColimit.isColimit_eq_iff _ hc' (xi := g' r) (j := i) (xj := (0 : F.obj i))
    suffices H : (g' ≫ c.ι.app i) r = 0 by
      obtain ⟨k, f, g, e⟩ := this.mp (by simpa using H)
      exact ⟨k, f, by simpa using e⟩
    rw [← hg']
    simp [show π r = 0 from hs.le (Ideal.subset_span r.2)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
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
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)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  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))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : (r : ↥s) → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' :
  ∀ (r : ↥s),
    Eq (α := (↑(F.obj (i' r)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map (hi' r)) :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj (i' r)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj (i' r)) : Type u))
      (0 : (↑(F.obj (i' r)) : Type u))
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have obtain : ∀ (c' : Cocone (WidePushoutShape.wideSpan i i' hi')),
  ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
Tactic: obtain ⟨c'⟩ := IsFiltered.cocone_nonempty (WidePushoutShape.wideSpan i i' hi')
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
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
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)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  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))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : (r : ↥s) → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' :
  ∀ (r : ↥s),
    Eq (α := (↑(F.obj (i' r)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map (hi' r)) :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj (i' r)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj (i' r)) : Type u))
      (0 : (↑(F.obj (i' r)) : Type u))
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ ∃ (i : J) (g' : S ⟶ F.obj i), (iP ≫ π) ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i
have refine_1 : LE.le (α := Ideal (↑P : Type u)) (ker (CommRingCat.Hom.hom π))
  (ker (F := (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u)) (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))
Tactic: refine ⟨c'.pt, CommRingCat.ofHom (RingHom.liftOfSurjective π.hom hπ
    ⟨(g' ≫ F.map (c'.ι.app none)).hom, ?_⟩), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FinitePresentation (goal)
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
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
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)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) (↑R : Type u))
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn :
  ∃ (f : MvPolynomial (Fin n) (↑R : Type u) →ₐ[(↑R : Type u)] (↑S : Type u)),
    Function.Surjective (α := MvPolynomial (Fin n) (↑R : Type u)) (β := (↑S : Type u))
        (⇑f : (a : MvPolynomial (Fin n) (↑R : Type u)) → (↑S : Type u)) ∧
      Ideal.FG (ker f.toRingHom)
hπ :
  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))
s : Finset (↑P : Type u)
hs : Eq (α := Ideal (↑P : Type u)) (Ideal.span (↑s : Set (↑P : Type u))) (ker (CommRingCat.Hom.hom π))
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : (r : ↥s) → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' :
  ∀ (r : ↥s),
    Eq (α := (↑(F.obj (i' r)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.map (hi' r)) :
            (a : (↑(F.obj i) : Type u)) → (↑(F.obj (i' r)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) g' :
                (a : (↑P : Type u)) → (↑(F.obj i) : Type u))
              (↑r : (↑P : Type u)) :
            (↑(F.obj i) : Type u)) :
        (↑(F.obj (i' r)) : Type u))
      (0 : (↑(F.obj (i' r)) : Type u))
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ LE.le (α := Ideal (↑P : Type u)) (ker (CommRingCat.Hom.hom π))
    (ker (F := (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u)) (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none))))
have refine_1 : (↑s : Set (↑P : Type u)) ⊆
  (↑(ker (F := (↑P : Type u) →+* (↑(F.1 c'.pt) : Type u)) (CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)))) :
    Set (↑P : Type u))
Tactic: rw [← hs, Ideal.span_le]