awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
R : CommRingCat
J : Type u
h : _root_.Finite J
A : Under R
h_1 :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres :
  ∀ (j : Discrete J), (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u)) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y := limit (J := Discrete J) (Discrete.functor fun (i : J) ↦ pres.diag.obj { as := i }))
      (HasLimit.isoOfNatIso (Discrete.natIso fun (i : Discrete J) ↦ eqToIso ⋯))
      (limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun (i : J) ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun (i : J) ↦ pres.diag.obj { as := i : Discrete J } }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
have rw : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
  (R.mkUnder ((i : J) → (↑(pres.diag.obj { as := i : Discrete J }).right : Type u))).hom
Tactic: rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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 := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj WalkingParallelPair
have refine : ∀ (A : Under R),
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
      WalkingParallelPair A →
    ∀ (pres : LimitPresentation WalkingParallelPair A)
      (hpres :
        ∀ (j : WalkingParallelPair),
          (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)),
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
Tactic: refine ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (hypothesis)
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
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
have this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
Tactic: have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
A : Under R
h :
  ObjectProperty.limitsOfShape (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
    WalkingParallelPair A
pres : LimitPresentation WalkingParallelPair A
hpres :
  ∀ (j : WalkingParallelPair),
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅
  R.mkUnder
    ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
        (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right))) :=
  Iso.trans (Y := limit pres.diag)
    (Iso.symm (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }))
    (Iso.trans (Y :=
      limit (parallelPair (pres.diag.map WalkingParallelPairHom.left) (pres.diag.map WalkingParallelPairHom.right)))
      (HasLimit.isoOfNatIso (diagramIsoParallelPair pres.diag))
      (limit.isoLimitCone
        {
          cone :=
            CommRingCat.Under.equalizerFork (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right),
          isLimit :=
            CommRingCat.Under.equalizerForkIsLimit (pres.diag.map WalkingParallelPairHom.left)
              (pres.diag.map WalkingParallelPairHom.right) }))
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
have rw : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
  (R.mkUnder
      ↥(AlgHom.equalizer (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.left))
          (CommRingCat.toAlgHom (pres.diag.map WalkingParallelPairHom.right)))).hom
Tactic: rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
R : CommRingCat
⊢ 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)
have refine : (J : Type u) →
  Fintype J →
    CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
      (Discrete J)
      (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
Tactic: refine .mk' _ fun (J : Type u) _ ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
R : CommRingCat
J : Type u
x : Fintype J
⊢ CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (Discrete J)
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
have 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))
  (Discrete J)
Tactic: apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (hypothesis)
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
R : CommRingCat
J : Type u
x : Fintype J
⊢ ObjectProperty.IsClosedUnderLimitsOfShape (C := Comma (Functor.fromPUnit R) (𝟭 CommRingCat))
    (commaObj (Functor.fromPUnit R) (𝟭 CommRingCat)
      (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (Discrete J)
have this : ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
  (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
Tactic: have := hQp.isClosedUnderLimitsOfShape hQi R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
R : CommRingCat
⊢ Limits.HasFiniteProducts.{u, u + 1} ((toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
have refine : ∀ (n : ℕ) (D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R),
  HasLimit D
Tactic: refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
R : CommRingCat
n : ℕ
D : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ HasLimit D
have have : ∀
  (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)),
  HasLimit D
Tactic: have := hQp.createsFiniteProductsForget hQi R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
⊢ PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
have have : ∀
  (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)),
  PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
Tactic: have := hQp.createsFiniteProductsForget hQi R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
⊢ PreservesFiniteProducts (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
have refine : ∀ (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)
Tactic: refine ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have rw : PreservesLimit K
  (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ⊤ R ⋙
    CategoryTheory.Under.pushout f)
Tactic: rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (hypothesis)
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)
have 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)
Tactic: have : PreservesLimit K (Under.pushout (toMorphismProperty Q) ⊤ f ⋙
        Under.forget (toMorphismProperty Q) ⊤ S) := by
    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
⊢ 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)
have 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
Tactic: apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have refine : ∀ (D : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R),
  HasLimit D
Tactic: refine ⟨fun D ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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
⊢ HasLimit D
have 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
Tactic: have := hQe.createsLimitsWalkingParallelPair hQi R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (hypothesis)
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 ι
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective (α := TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)))
      (β :=
      ↥(AlgHom.equalizer (F :=
          TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
            TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g) :
            TensorProduct (↑R : Type u) (↑S : Type u) (↑A.right : Type u) →ₐ[(↑R : Type u)]
              TensorProduct (↑R : Type u) (↑S : Type u) (↑B.right : Type u))))
      (⇑(AlgHom.tensorEqualizer (↑R : Type u) (↑S : Type u) (toAlgHom f) (toAlgHom g)) :
        (a : TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) →
          ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom f))
              (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (toAlgHom g))))
have w' : 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))
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [Fork.IsLimit.lift_ι]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
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)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: dsimp