awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
h :
  pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)
⊢ Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
          Under.homMk
            (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
              (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
            ⋯)
have h₁ : pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
  pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
    Under.Hom.right
      (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
        Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
          Under.homMk
            (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
              (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) sorry)
            sorry)
Tactic: apply pushout.hom_ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)
have h : (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
    Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
  (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) sorry)
              sorry)) ≫
    Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
Tactic: rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
have h : ∀ (x : (↑A.right : Type u)),
  Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑A.right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inl A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                      Under.homMk
                        (pushout.desc
                          (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) sorry)
                        sorry)) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑A.right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫ (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B)) =
    pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
              ⋯)
have h : (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
    Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
  (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
      Under.Hom.right
        (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
          Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) sorry)
              sorry)) ≫
    Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
Tactic: rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Basic (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f : A ⟶ B
⊢ (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B)) =
    (pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
        Under.Hom.right
          (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
            Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                  (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) ⋯)
                ⋯)) ≫
      Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))
have h : ∀ (x : (↑S : Type u)),
  Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    (R.tensorProd S).map f ≫ Iso.hom (tensorProdObjIsoPushoutObj S B))) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑(of (↑S : Type u)) : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
    ((Hom.hom
            ((pushout.inr A.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ≫
                Under.Hom.right
                  (Iso.inv (tensorProdObjIsoPushoutObj S A) ≫
                    Iso.hom (tensorProdObjIsoPushoutObj S A) ≫
                      Under.homMk
                        (pushout.desc
                          (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
                          (pushout.inr B.hom (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))) sorry)
                        sorry)) ≫
              Under.Hom.right (Iso.inv (tensorProdObjIsoPushoutObj S B))) :
          (a : (↑(of (↑S : Type u)) : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
        x :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑B.right : Type u))).right : Type u))
Tactic: ext (x : S)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
⊢ Eq (α :=
    Cone.pt (F := Discrete.functor fun (i : ι) ↦ S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
        (tensorProductFan S P) ⟶
      S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
    (Fan.proj (tensorProductFan S P) i)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := Discrete.functor fun (i : ι) ↦ S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
        (tensorProductFan' S P))
      (Iso.hom
        (AlgEquiv.toUnder
          (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
            (↑(P i).right : Type u))))
      (Fan.proj (tensorProductFan' S P) i))
have dsimp : Eq.{u + 1} (α :=
  S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u))) ⟶
    S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
  (AlgHom.toUnder
    (Algebra.TensorProduct.map (AlgHom.id (↑S : Type u) (↑S : Type u))
      (Pi.evalAlgHom (↑R : Type u) (fun (j : ι) ↦ (↑(P j).right : Type u)) i)))
  (CategoryStruct.comp (Y := S.mkUnder ((i : ι) → (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)))
    (Iso.hom
      (AlgEquiv.toUnder
        (Algebra.TensorProduct.piRight (↑R : Type u) (↑S : Type u) (↑S : Type u) fun (i : ι) ↦
          (↑(P i).right : Type u))))
    (AlgHom.toUnder
      (Pi.evalAlgHom (↑S : Type u) (fun (i : ι) ↦ (↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u)) i)))
Tactic: dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ Eq (α := R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ B)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g)
have h : ∀ (a : ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))),
  Eq (α := (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))).right)
            (Under.Hom.right (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f)) :
          (a : (↑(R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))).right : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))).right)
            (Under.Hom.right (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g)) :
          (a : (↑(R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))).right : Type u)) → (↑B.right : Type u))
        a :
      (↑B.right : Type u))
Tactic: ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
⊢ Eq (α := R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ B)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g)
have rw : Eq (α := R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ B)
  (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g)
  (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g)
Tactic: rw [equalizer_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Type u
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra (↑R : Type u) A
inst_4 : Algebra (↑R : Type u) B
f g : A →ₐ[(↑R : Type u)] B
⊢ Eq (α := R.mkUnder ↥(AlgHom.equalizer f g) ⟶ R.mkUnder B)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer f g)) ≫ f.toUnder)
    (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer f g)) ≫ g.toUnder)
have h : ∀ (a : ↥(AlgHom.equalizer f g)),
  Eq (α := (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (R.mkUnder ↥(AlgHom.equalizer f g)).right)
            (Under.Hom.right (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer f g)) ≫ f.toUnder)) :
          (a : (↑(R.mkUnder ↥(AlgHom.equalizer f g)).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (R.mkUnder ↥(AlgHom.equalizer f g)).right)
            (Under.Hom.right (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer f g)) ≫ g.toUnder)) :
          (a : (↑(R.mkUnder ↥(AlgHom.equalizer f g)).right : Type u)) → (↑(R.mkUnder B).right : Type u))
        a :
      (↑(R.mkUnder B).right : Type u))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
⊢ Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map f)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
have rw : Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f))
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
    (R.tensorProd S).map g)
Tactic: rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
rw :
  Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f))
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
⊢ Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map f)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
have rw₁ : Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g))
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
    (R.tensorProd S).map g)
Tactic: rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
rw :
  Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ f))
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
rw₁ :
  Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ≫ g))
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
⊢ Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map f)
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
      (R.tensorProd S).map g)
have rw₂ : Eq (α := (R.tensorProd S).obj (R.mkUnder ↥(AlgHom.equalizer (toAlgHom f) (toAlgHom g))) ⟶ (R.tensorProd S).obj B)
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
    (R.tensorProd S).map g)
  ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))) ≫
    (R.tensorProd S).map g)
Tactic: rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Under.Limits (goal)
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
inst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
⊢ 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
-- 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
⊢ ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj
have refine : ∀ (J : Type u),
  _root_.Finite J →
    ∀ (A : Under R),
      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)),
          (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A
Tactic: refine .of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨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
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 } }))
⊢ (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