awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 x
-- 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) ⋯
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)
have h₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext x
-- 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 ι
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) ⋯
⊢ IsIso (IsLimit.lift (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (Fork.ofι h' w')) ↔
    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 heq : 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
-- 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) ⋯
heq : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsIso (IsLimit.lift (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (Fork.ofι h' w')) ↔
    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 rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
    ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)
have rw : Function.Bijective (α :=
  TensorProduct (↑R : Type u) (↑S : Type u) ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.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)) (CommRingCat.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)) (CommRingCat.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) (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g)) :
    (a :
        TensorProduct (↑R : Type u) (↑S : Type u)
          ↥(AlgHom.equalizer (CommRingCat.toAlgHom f) (CommRingCat.toAlgHom g))) →
      ↥(AlgHom.equalizer (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom f))
          (Algebra.TensorProduct.map (AlgHom.id (↑R : Type u) (↑S : Type u)) (CommRingCat.toAlgHom g))))
Tactic: rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
⊢ PreservesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
have refine : ∀ {K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R},
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
Tactic: refine ⟨fun {K} ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
have have : ∀
  (this :
    CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
      WalkingParallelPair
      (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)),
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
Tactic: have := hPe.createsLimitsWalkingParallelPair hPi R
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
have rw : PreservesLimit
  (parallelPair
    ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
      WalkingParallelPairHom.left)
    ((K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R).map
      WalkingParallelPairHom.right))
  (R.tensorProd S)
Tactic: rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
have this₁ : PreservesLimit
  (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
  (CategoryTheory.Under.pushout f)
Tactic: have : PreservesLimit (K ⋙ Under.forget (toMorphismProperty P) ⊤ R)
      (CategoryTheory.Under.pushout f) := by
    rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
    exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Property (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)
have rw : PreservesLimit K
  (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ 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:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
inst : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this_1 :
  CreatesLimitsOfShape (C := (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).Under ⊤ R)
    WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this :
  PreservesLimit
    (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)
⊢ PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f)
have this₁ : PreservesLimit K
  (MorphismProperty.Under.pushout (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ f ⋙
    MorphismProperty.Under.forget (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ⊤ S)
Tactic: have : PreservesLimit K (Under.pushout (toMorphismProperty P) ⊤ f ⋙
        Under.forget (toMorphismProperty P) ⊤ S) := by
    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Category.Semigrp.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) = MulHom.id (↑X : Type u_1)
have h : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑X : Type u_1))
    (((MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Semigrp.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) = MulHom.id (↑Y : Type u_1)
have h : ∀ (x : (↑Y : Type u_1)),
  Eq (α := (↑Y : Type u_1))
    (((MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Semigrp.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) = MulHom.id (↑X : Type u_1)
have h : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑X : Type u_1))
    (((Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x :
      (↑X : Type u_1))
    ((MulHom.id (↑X : Type u_1) : (a : (↑X : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Semigrp.Basic (goal)
Goal:
X_1 Y_1 : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) = MulHom.id (↑Y : Type u_1)
have h : ∀ (x : (↑Y : Type u_1)),
  Eq (α := (↑Y : Type u_1))
    (((Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x :
      (↑Y : Type u_1))
    ((MulHom.id (↑Y : Type u_1) : (a : (↑Y : Type u_1)) → (↑Y : Type u_1)) x : (↑Y : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (goal)
Goal:
K : Type u
inst : CommSemiring K
D : Type v
inst_1 : Semiring D
inst_2 : Algebra K D
h : IsCentral K D
x : D
⊢ Membership.mem (γ := Subalgebra K D) (Subalgebra.center K D) x ↔ ∃ (a : K), x = (algebraMap K D : (a : K) → D) a
have rw : Membership.mem (γ := Set D) (Set.range.{v, u + 1} (ι := K) (⇑(algebraMap K D) : (a : K) → D)) x ↔
  ∃ (a : K), x = (algebraMap K D : (a : K) → D) a
Tactic: rw [center_eq_bot, Algebra.mem_bot]
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (goal)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
x : D
⊢ Membership.mem (γ := Subalgebra k D) (Subalgebra.center k D) x → Membership.mem (γ := Subalgebra K D) ⊥ x
have simp : ∀ (x_1 : k) (h : (algebraMap k D : (a : k) → D) x_1 = x), ∃ (y : K), (algebraMap K D : (a : K) → D) y = x
Tactic: simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)
have this : IsCentral K D
Tactic: haveI : IsCentral K D :=
  { out := fun x ↦ show x ∈ Subalgebra.center k D → _ by
      simp only [center_eq_bot, mem_bot, Set.mem_range, forall_exists_index]
      rintro x rfl
      exact ⟨algebraMap k K x, by simp [algebraMap_eq_smul_one, smul_assoc]⟩ }
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (goal)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
this : IsCentral K D
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := k) (β := K) (⇑(algebraMap k K) : (a : k) → K)
have refine : ∀ (x : K), ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
Tactic: refine ⟨FaithfulSMul.algebraMap_injective k K, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
this : IsCentral K D
x : K
⊢ ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
have H : Membership.mem (α := D) (↑(Subalgebra.center K D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
Tactic: have H : algebraMap K D x ∈ (Subalgebra.center K D : Set D) := Subalgebra.algebraMap_mem _ _
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
this : IsCentral K D
x : K
H : Membership.mem (α := D) (↑(Subalgebra.center K D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
⊢ ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
have H₁ : Membership.mem (α := D) (↑(Subalgebra.center k D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
Tactic: rw [show (Subalgebra.center K D : Set D) = Subalgebra.center k D by rfl] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Central.Basic (hypothesis)
Goal:
k : Type u_1
K : Type u_2
D : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Ring D
inst_3 : Nontrivial D
inst_4 : Algebra k K
inst_5 : Algebra K D
inst_6 : Algebra k D
inst_7 : IsScalarTower k K D
inst_8 : IsCentral k D
this : IsCentral K D
x : K
H : Membership.mem (α := D) (↑(Subalgebra.center k D) : Set D) ((algebraMap K D : (a : K) → D) x : D)
⊢ ∃ (a : k), (algebraMap k K : (a : k) → K) a = x
have H₁ : ∃ (y : k), Eq.{u_3 + 1} (α := D) ((algebraMap k D : (a : k) → D) y : D) ((algebraMap K D : (a : K) → D) x : D)
Tactic: simp only [center_eq_bot, coe_bot, Set.mem_range] at H
Cleared hypotheses: H