awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)
preserves :
  ∀ (i : J) (g : S.right ⟶ (F ⋙ Under.forget R).obj i)
    (h₁ : S.hom ≫ g = NatTrans.app { app := fun (i : J) ↦ (F.obj i).hom, naturality := ⋯ } i)
    (h₂ : Under.Hom.right f = g ≫ NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget R) c)) i),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
      f =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
          xi
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi

Tactic:
obtain ⟨i, g, h₁, h₂⟩ := RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit
       R (F ⋙ Under.forget R) { app i := (F.obj i).hom } S.hom ((Under.forget R).mapCocone c)
      (PreservesColimit.preserves hc).some hS f.right (by simp)

Premises used: CategoryTheory.Functor.mapCocone, RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit, CategoryTheory.Functor.comp, CategoryTheory.Under.hom, Nonempty.some, CategoryTheory.Limits.PreservesColimit.preserves, CategoryTheory.Under.forget, CategoryTheory.NatTrans.mk, CategoryTheory.Under.Hom.right, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)
i : J
g : S.right ⟶ (F ⋙ Under.forget R).obj i
h₁ : S.hom ≫ g = NatTrans.app { app := fun (i : J) ↦ (F.obj i).hom, naturality := ⋯ } i
h₂ : Under.Hom.right f = g ≫ NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget R) c)) i
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi

Tactic:
⟨i, Under.homMk g h₁, Under.UnderMorphism.ext h₂⟩

Premises used: CategoryTheory.Under.homMk, CategoryTheory.Under.UnderMorphism.ext, Exists.intro
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
f :
  Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S)) (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)
i : J
g : S.right ⟶ (F ⋙ Under.forget R).obj i
h₁ : S.hom ≫ g = NatTrans.app { app := fun (i : J) ↦ (F.obj i).hom, naturality := ⋯ } i
h₂ : Under.Hom.right f = g ≫ NatTrans.app (Cocone.ι (Functor.mapCocone (Under.forget R) c)) i
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i)),
    f =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        xi

Tactic:
exact ⟨i, Under.homMk g h₁, Under.UnderMorphism.ext h₂⟩
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
J : Type uJ
inst : Category.{vJ, uJ} J
inst_1 : IsFiltered.{vJ, uJ} J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : CategoryTheory.Functor.{vJ, u, uJ, u + 1} J (Under R)
inst_2 :
  PreservesColimit (F ⋙ Under.forget R)
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ Functor.obj coyoneda (Opposite.op S)).obj i
f₂ : (F ⋙ Functor.obj coyoneda (Opposite.op S)).obj j
e_1 :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj.{vJ, u, uJ, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
            (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
        i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj i))
        f₁ :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{vJ, u, uJ, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
          i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (Opposite.op S)).mapCocone c).pt).obj j))
        f₂ :
      (fun (X : Type u) ↦ X)
        (Functor.obj.{vJ, u, uJ, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (Opposite.op S))
              (Functor.mapCocone (Functor.obj coyoneda (Opposite.op S)) c)))
          j))
k : J
hik : i ⟶ k
hjk : j ⟶ k
e : Under.Hom.right f₁ ≫ (F ⋙ Under.forget R).map hik = Under.Hom.right f₂ ≫ (F ⋙ Under.forget R).map hjk
⊢ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).map f) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj k))
          f₁ :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).map g) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj k))
          f₂ :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (Opposite.op S)).obj k))

Tactic:
exact ⟨k, hik, hjk, Under.UnderMorphism.ext e⟩
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ PreservesFilteredColimits (Functor.obj coyoneda (Opposite.op S))

Tactic:
⟨fun _ _ _ ↦ ⟨preservesColimit_coyoneda_of_finitePresentation R S hS _⟩⟩

Premises used: CategoryTheory.Limits.PreservesFilteredColimitsOfSize.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk, CommRingCat.preservesColimit_coyoneda_of_finitePresentation
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
rw : PreservesFilteredColimits (Functor.obj coyoneda (Opposite.op S))
⊢ IsFinitelyPresentable S

Tactic:
rw [isFinitelyPresentable_iff_preservesFilteredColimits]

Premises used: CategoryTheory.isFinitelyPresentable_iff_preservesFilteredColimits
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ PreservesFilteredColimits (Functor.obj coyoneda (Opposite.op S))

Tactic:
preservesFilteredColimits_coyoneda R S hS

Premises used: CommRingCat.preservesFilteredColimits_coyoneda
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ PreservesFilteredColimits (Functor.obj coyoneda (Opposite.op S))

Tactic:
exact preservesFilteredColimits_coyoneda R S hS

Premises used: CommRingCat.preservesFilteredColimits_coyoneda
-- Module: Mathlib.Algebra.Category.Ring.FinitePresentation
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FinitePresentation
⊢ MorphismProperty.isFinitelyPresentable CommRingCat f

Tactic:
isFinitelyPresentable_under R (Under.mk f) hf

Premises used: CategoryTheory.MorphismProperty.isFinitelyPresentable, CategoryTheory.Under.mk, CommRingCat.isFinitelyPresentable_under, CategoryTheory.ObjectProperty.isFinitelyPresentable
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R : CommRingCat
⊢ IsIso.{u_1, u_1 + 1} (X := CommRingCat.of (↑R : Type u_1)) (Y :=
    CommRingCat.of (Localization.Away (M := (↑R : Type u_1)) 1))
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away (M := (↑R : Type u_1)) 1)))

Tactic:
Iso.isIso_hom (IsLocalization.atOne R (Localization.Away (1 : R))).toRingEquiv.toCommRingCatIso

Premises used: CommRingCat.carrier, RingEquiv.toCommRingCatIso, Localization.Away, MonoidHomClass.toMonoidHom, IsLocalization.atOne, CategoryTheory.Iso.isIso_hom, Quotient.mk', RingHomClass.toRingHom, AlgEquiv.toRingEquiv, OfNat.ofNat, OreLocalization.oreDiv
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R : CommRingCat
of :
  ∀ (carrier : Type u_1) [commRing : CommRing carrier],
    IsIso.{u_1, u_1 + 1} (X := CommRingCat.of carrier) (Y :=
      CommRingCat.of (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1))
      (CommRingCat.ofHom
        (algebraMap (↑(CommRingCat.of carrier) : Type u_1)
          (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1)))
⊢ IsIso.{u_1, u_1 + 1} (X := R) (Y := CommRingCat.of (Localization.Away (M := (↑R : Type u_1)) 1))
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away (M := (↑R : Type u_1)) 1)))

Tactic:
cases R
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
carrier : Type u_1
commRing : CommRing carrier
⊢ IsIso.{u_1, u_1 + 1} (X := CommRingCat.of carrier) (Y :=
    CommRingCat.of (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1))
    (CommRingCat.ofHom
      (algebraMap (↑(CommRingCat.of carrier) : Type u_1)
        (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1)))

Tactic:
localization_unit_isIso _

Premises used: localization_unit_isIso
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
carrier : Type u_1
commRing : CommRing carrier
⊢ IsIso.{u_1, u_1 + 1} (X := CommRingCat.of carrier) (Y :=
    CommRingCat.of (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1))
    (CommRingCat.ofHom
      (algebraMap (↑(CommRingCat.of carrier) : Type u_1)
        (Localization.Away (M := (↑(CommRingCat.of carrier) : Type u_1)) 1)))

Tactic:
exact localization_unit_isIso _

Premises used: localization_unit_isIso
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_1
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Epi (X := CommRingCat.of R) (Y := CommRingCat.of S) (CommRingCat.ofHom (algebraMap R S))

Tactic:
⟨fun _ _ h => CommRingCat.hom_ext <| ringHom_ext M congr(($h).hom)⟩

Premises used: CommRingCat.hom_ext, CommRingCat.Hom.hom, congrArg, id, CategoryTheory.Epi.mk, IsLocalization.ringHom_ext
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
⊢ Epi (X := CommRingCat.of R) (Y := CommRingCat.of (Localization (M := R) M))
    (CommRingCat.ofHom (algebraMap R (Localization (M := R) M)))

Tactic:
IsLocalization.epi M _

Premises used: IsLocalization.epi
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R : CommRingCat
M : Submonoid (↑R : Type u_1)
rcases :
  ∀ (α : Type u_1) [commRing : CommRing α] (M : Submonoid (↑(CommRingCat.of α) : Type u_1)),
    Epi.{u_1, u_1 + 1} (X := CommRingCat.of α) (Y := CommRingCat.of (Localization M))
      (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of α) : Type u_1) (Localization M)))
⊢ Epi.{u_1, u_1 + 1} (X := R) (Y := CommRingCat.of (Localization M))
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization M)))

Tactic:
rcases R with ⟨α, str⟩
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
α : Type u_1
commRing : CommRing α
M : Submonoid (↑(CommRingCat.of α) : Type u_1)
⊢ Epi.{u_1, u_1 + 1} (X := CommRingCat.of α) (Y :=
    CommRingCat.of (Localization (M := (↑(CommRingCat.of α) : Type u_1)) M))
    (CommRingCat.ofHom
      (algebraMap (↑(CommRingCat.of α) : Type u_1) (Localization (M := (↑(CommRingCat.of α) : Type u_1)) M)))

Tactic:
IsLocalization.epi M _

Premises used: IsLocalization.epi
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
α : Type u_1
commRing : CommRing α
M : Submonoid (↑(CommRingCat.of α) : Type u_1)
⊢ Epi.{u_1, u_1 + 1} (X := CommRingCat.of α) (Y :=
    CommRingCat.of (Localization (M := (↑(CommRingCat.of α) : Type u_1)) M))
    (CommRingCat.ofHom
      (algebraMap (↑(CommRingCat.of α) : Type u_1) (Localization (M := (↑(CommRingCat.of α) : Type u_1)) M)))

Tactic:
exact IsLocalization.epi M _

Premises used: IsLocalization.epi
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst : IsLocalHom (R := (↑S : Type u_1)) (S := (↑T : Type u_1)) (Hom.hom g)
inst_1 : IsLocalHom (R := (↑R : Type u_1)) (S := (↑S : Type u_1)) (Hom.hom f)
⊢ IsLocalHom (R := (↑R : Type u_1)) (S := (↑T : Type u_1)) (Hom.hom (f ≫ g))

Tactic:
RingHom.isLocalHom_comp _ _

Premises used: RingHom.isLocalHom_comp
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R S : CommRingCat
f : R ≅ S
a : (↑R : Type u_1)
ha :
  IsUnit (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
⊢ IsUnit (M := (↑R : Type u_1))
    ((CommRingCat.Hom.hom f.inv : (a : (↑S : Type u_1)) → (↑R : Type u_1))
        ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1)) :
      (↑R : Type u_1))

Tactic:
f.inv.hom.isUnit_map ha

Premises used: CommRingCat.Hom.hom, RingHom.isUnit_map, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R S : CommRingCat
f : R ≅ S
a : (↑R : Type u_1)
ha :
  IsUnit (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
h :
  a =
    (CommRingCat.Hom.hom f.inv : (a : (↑S : Type u_1)) → (↑R : Type u_1))
      ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
⊢ IsUnit a

Tactic:
convert! f.inv.hom.isUnit_map ha

Premises used: CommRingCat.Hom.hom, RingHom.isUnit_map, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R S : CommRingCat
f : R ≅ S
a : (↑R : Type u_1)
ha :
  IsUnit (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))
⊢ a =
    (CommRingCat.Hom.hom f.inv : (a : (↑S : Type u_1)) → (↑R : Type u_1))
      ((CommRingCat.Hom.hom f.hom : (a : (↑R : Type u_1)) → (↑S : Type u_1)) a : (↑S : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Instances
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
⊢ IsLocalHom (R := (↑R : Type u_1)) (S := (↑S : Type u_1)) (CommRingCat.Hom.hom f)

Tactic:
isLocalHom_of_iso (asIso f)

Premises used: isLocalHom_of_iso, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
x x_1 : J
f : x ⟶ x_1
hf :
  ∀
    (x_2 :
      (↑(Functor.obj.{w, u, v, u + 1}
            (Functor.obj (Functor.const J)
              (of
                (Types.Small.limitCone
                    (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier))).pt))
            x) :
        Type u)),
    Eq (α := (↑(F.obj x_1) : Type u))
      ((Hom.hom
              (CategoryTheory.Functor.map
                  (Functor.obj (Functor.const J)
                    (of
                      (Types.Small.limitCone
                          (F ⋙
                            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := carrier))).pt))
                  f ≫
                ofHom (limitπRingHom F x_1)) :
            (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
              (↑(F.obj x_1) : Type u))
          x_2 :
        (↑(F.obj x_1) : Type u))
      ((Hom.hom (ofHom (limitπRingHom F x) ≫ F.map f) :
            (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
              (↑(F.obj x_1) : Type u))
          x_2 :
        (↑(F.obj x_1) : Type u))
⊢ Eq (α :=
    Functor.obj.{w, u, v, u + 1}
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        f ≫
      ofHom (limitπRingHom F x_1))
    (ofHom (limitπRingHom F x) ≫ F.map f)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
x x_1 : J
f : x ⟶ x_1
x_2 :
  (↑(Functor.obj.{w, u, v, u + 1}
        (Functor.obj (Functor.const J)
          (of
            (Types.Small.limitCone
                (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier))).pt))
        x) :
    Type u)
⊢ Eq (α := (↑(F.obj x_1) : Type u))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of
                    (Types.Small.limitCone
                        (F ⋙
                          forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := carrier))).pt))
                f ≫
              ofHom (limitπRingHom F x_1)) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))
    ((Hom.hom (ofHom (limitπRingHom F x) ≫ F.map f) :
          (a : (↑(((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget SemiRingCat)).pt)).obj x) : Type u)) →
            (↑(F.obj x_1) : Type u))
        x_2 :
      (↑(F.obj x_1) : Type u))

Tactic:
simpa using (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.Small.limitCone, CategoryTheory.Functor.comp, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
s : Cone F
⊢ Eq.{u + 1} (α :=
    Shrink.{u, max u v}
      (↑(F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
    ((equivShrink
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)) :
          (a : (↑(F ⋙ forget SemiRingCat).sections : Type (max u v))) →
            Shrink.{u, max u v} (↑(F ⋙ forget SemiRingCat).sections : Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (F.obj j)) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦ 1) ⋯) :
      Shrink.{u, max u v}
        (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)))
    (1 :
      (Types.Small.limitCone
          (F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier))).pt)

Tactic:
rfl