awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
x : (↑S : Type u)
y : (i : ι) → (↑(P i).right : Type u)
⊢ Eq (α := (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (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)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        (x ⊗ₜ[(↑R : Type u)] y) :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (X :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right) (Y :=
            (S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right)
            (Under.Hom.right
              (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)))) :
          (a : (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] ((i : ι) → (↑(P i).right : Type u)))).right : Type u)) →
            (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))
        (x ⊗ₜ[(↑R : Type u)] y) :
      (↑(S.mkUnder ((↑S : Type u) ⊗[(↑R : Type u)] (↑(P i).right : Type u))).right : Type u))

Tactic:
simp only [AlgHom.toUnder_right, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        Pi.evalAlgHom_apply, Under.comp_right, comp_apply, AlgEquiv.toUnder_hom_right_apply,
        Algebra.TensorProduct.piRight_tmul]

Premises used: AlgHom.coe_id, Algebra.TensorProduct.map_tmul, AlgHom.toUnder_right, AlgEquiv.toUnder_hom_right_apply, Algebra.TensorProduct.piRight_tmul, CommRingCat.comp_apply, Pi.evalAlgHom_apply, id_eq, CategoryTheory.Under.comp_right
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
ι : Type u
P : ι → Under R
J : Type u
inst_1 : Finite J
f : J → Under R
⊢ PreservesLimit (Discrete.functor f) (R.tensorProd S)

Tactic:
let c : Fan _ := Under.piFan f
  have hc : IsLimit c := Under.piFanIsLimit f
  preservesLimit_of_preserves_limit_cone hc (piFanTensorProductIsLimit f)

Premises used: CommRingCat.Under.piFan, CommRingCat.Under.piFanIsLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CommRingCat.Under.piFanTensorProductIsLimit
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R : CommRingCat
A B : Under R
f g : A ⟶ B
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))
⊢ 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)

Tactic:
ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))

Premises used: AlgHom.equalizer, CommRingCat.toAlgHom
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R : CommRingCat
A B : Under R
f g : A ⟶ B
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:
a.property

Premises used: Set.Mem, setOf, Subtype.property
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R : CommRingCat
A B : Under R
f g : A ⟶ B
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:
exact a.property

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
rw 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)
⊢ 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)

Tactic:
rw [equalizer_comp]

Premises used: CommRingCat.Under.equalizer_comp
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ (equalizerFork f g).ι = AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, Set.Mem, CategoryTheory.Under.homMk, AlgHom.toUnder, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
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))
⊢ 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)

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
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:
a.property

Premises used: Set.Mem, setOf, Subtype.property
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
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:
exact a.property

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R : CommRingCat
A B : Type u
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra (↑R : Type u) A
inst_3 : Algebra (↑R : Type u) B
f g : A →ₐ[(↑R : Type u)] B
⊢ (equalizerFork' f g).ι = AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer f g))

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, Set.Mem, CategoryTheory.Under.homMk, AlgHom.toUnder, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [← Functor.map_comp, equalizer_comp, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CommRingCat.Under.equalizer_comp
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
A B : Under R
f g : A ⟶ B
⊢ Eq (α :=
    Cone.pt (F := parallelPair ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (tensorProdEqualizer f g) ⟶
      (R.tensorProd S).obj A)
    (Fork.ι (tensorProdEqualizer f g))
    ((R.tensorProd S).map (AlgHom.toUnder (Subalgebra.val (AlgHom.equalizer (toAlgHom f) (toAlgHom g)))))

Tactic:
rfl

Premises used: CategoryTheory.StructuredArrow.homMk, Set.Mem, CategoryTheory.Under.homMk, CommRingCat.mkUnder, CategoryTheory.Under.mk, CategoryTheory.Under, AlgHom.toUnder, CategoryTheory.Limits.Fork.ι, CategoryTheory.StructuredArrow.mk, CategoryTheory.StructuredArrow, rfl
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
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
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
x :
  (↑(Under.right (X := S)
        (Cone.pt (F := parallelPair ((R.tensorProd S).map f) ((R.tensorProd S).map g)) (tensorProdEqualizer f g))) :
    Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply AlgHom.coe_tensorEqualizer

Premises used: AlgHom.coe_tensorEqualizer
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
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
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)

Tactic:
let c : Fork f g := Under.equalizerFork f g
  let hc : IsLimit c := Under.equalizerForkIsLimit f g
  let hc' : IsLimit ((tensorProd R S).mapCone c) :=
    tensorProdMapEqualizerForkIsLimit f g
  preservesLimit_of_preserves_limit_cone hc hc'

Premises used: CommRingCat.Under.equalizerForkIsLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CommRingCat.Under.tensorProdMapEqualizerForkIsLimit, CommRingCat.Under.equalizerFork
-- Module: Mathlib.Algebra.Category.Ring.Under.Limits
Goal:
R S : CommRingCat
inst : Algebra (↑R : Type u) (↑S : Type u)
inst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ PreservesFiniteLimits (R.tensorProd S)

Tactic:
preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts (tensorProd R S)

Premises used: CommRingCat.tensorProd, CategoryTheory.Limits.preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts
-- 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
R : CommRingCat
⊢ ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj

Tactic:
.of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩

Premises used: _private.0.RingHom.HasFiniteProducts.isClosedUnderLimitsOfShape.match_1, CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.of_isClosedUnderLimitsOfShape, CategoryTheory.MorphismProperty.underObj, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk, RingHom.toMorphismProperty
-- 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
R : CommRingCat
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
⊢ ObjectProperty.IsClosedUnderFiniteProducts (C := Under R)
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj

Tactic:
refine .of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
-- 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
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)
i : Discrete J
⊢ pres.diag.obj i = Functor.obj (Discrete.functor fun (i : J) ↦ pres.diag.obj { as := i }) i

Tactic:
simp
-- 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
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).RespectsIso

Tactic:
have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
-- 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
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
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
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]

Premises used: RingHom.toMorphismProperty, CategoryTheory.MorphismProperty.underObj_iff, CategoryTheory.Iso.inv, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso, CategoryTheory.Under.w