awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
rw :
  PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R ⋙
      CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ S)

Tactic:
rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]

Premises used: CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso, CategoryTheory.Limits.preservesLimit_iff_of_natIso
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ PreservesLimit K
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R ⋙
      CategoryTheory.Under.pushout f)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ S)

Tactic:
have : PreservesLimit K (Under.pushout (toMorphismProperty Q) ⊤ f ⋙
        Under.forget (toMorphismProperty Q) ⊤ S) := by
    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
    infer_instance
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this_1 :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ S)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
preservesLimit_of_reflects_of_preserves _ (MorphismProperty.Under.forget _ ⊤ S)

Premises used: CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this_1 :
  CreatesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ S)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
exact preservesLimit_of_reflects_of_preserves _ (MorphismProperty.Under.forget _ ⊤ S)

Premises used: CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CategoryTheory.MorphismProperty.Under.forget, Top.top
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
inst :
  ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    WalkingParallelPair
⊢ CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)

Tactic:
apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed

Premises used: CategoryTheory.MorphismProperty.Comma.forgetCreatesLimitsOfShapeOfClosed
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    WalkingParallelPair

Tactic:
hQe.isClosedUnderLimitsOfShape hQi _

Premises used: CategoryTheory.MorphismProperty.underObj, CategoryTheory.MorphismProperty.commaObj, RingHom.HasEqualizers.isClosedUnderLimitsOfShape, CategoryTheory.Under, CategoryTheory.Under.Hom, RingHom.toMorphismProperty, CategoryTheory.StructuredArrow
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    WalkingParallelPair

Tactic:
exact hQe.isClosedUnderLimitsOfShape hQi _

Premises used: RingHom.HasEqualizers.isClosedUnderLimitsOfShape
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ Limits.HasEqualizers.{u, u + 1} ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
⟨fun D ↦ ?_⟩

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
refine :
  ∀ (D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R),
    HasLimit D
⊢ Limits.HasEqualizers.{u, u + 1} ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
refine ⟨fun D ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
have :
  ∀
    (this :
      CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
        WalkingParallelPair
        (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)),
    HasLimit D
⊢ HasLimit D

Tactic:
have := hQe.createsLimitsWalkingParallelPair hQi R
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D

Tactic:
hasLimit_of_created D (Under.forget _ _ R)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.MorphismProperty.Under.forget
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ HasLimit D

Tactic:
exact hasLimit_of_created D (Under.forget _ _ R)

Premises used: CategoryTheory.hasLimit_of_created, CategoryTheory.MorphismProperty.Under.forget
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQp : RingHom.HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQe : RingHom.HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ HasFiniteLimits.{u, u + 1} ((RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
have := hQp.hasFiniteProducts hQi
  have := hQe.hasEqualizers hQi
  hasFiniteLimits_of_hasEqualizers_and_finite_products

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products, RingHom.HasEqualizers.hasEqualizers, RingHom.HasFiniteProducts.hasFiniteProducts
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
⊢ h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g

Tactic:
simpa using congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
⊢ h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g

Tactic:
have w' : h' ≫ (tensorProd R S).map f = h' ≫ (tensorProd R S).map g := by
    simpa using congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_

Premises used: CommRingCat.Under.equalizerForkIsLimit, CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_

Premises used: CommRingCat.Under.equalizerForkIsLimit, CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [Fork.IsLimit.lift_ι]

Premises used: CategoryTheory.Limits.Fork.IsLimit.lift_ι
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext : 2
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : (↑S : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
x : (↑(R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))).right : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Property
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
  AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
h' : (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
        Under.homMk (CommRingCat.ofHom (.id _)) := by
    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
    rw [Fork.IsLimit.lift_ι]
    ext : 2
    dsimp
    ext x <;> rfl