awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
inst_2 : Algebra R A
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ ∃ (P : FGAlgCatSkeleton R),
    Nonempty
      (A ≃ₐ[R] (↑((FGAlgCatSkeleton.eval R P).obj (P := fun (A : CommAlgCat R) ↦ FiniteType R (↑A : Type u))) : Type u))

Tactic:
⟨⟨n, RingHom.ker f⟩, ⟨(Ideal.quotientKerAlgEquivOfSurjective hf).symm⟩⟩

Premises used: AlgEquiv.symm, Nonempty.intro, FGAlgCatSkeleton.mk, Exists.intro, RingHom.ker, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
inst_2 : Algebra R A
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
⊢ ∃ (P : FGAlgCatSkeleton R),
    Nonempty
      (A ≃ₐ[R] (↑((FGAlgCatSkeleton.eval R P).obj (P := fun (A : CommAlgCat R) ↦ FiniteType R (↑A : Type u))) : Type u))

Tactic:
exact ⟨⟨n, RingHom.ker f⟩, ⟨(Ideal.quotientKerAlgEquivOfSurjective hf).symm⟩⟩
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ Algebra.FiniteType R S

Tactic:
algebraize [f]
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
obtain :
  ∀ (T : FGAlgCatSkeleton R)
    (e :
      S ≃ₐ[R]
        (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) :
          Type u)),
    ∃ (T : FGAlgCatSkeleton R) (e :
      RingEquiv.{u, v}
        (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
        S),
      f =
        e.toRingHom.comp
          (algebraMap R
            (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) :
              Type u))
⊢ ∃ (T : FGAlgCatSkeleton R) (e :
    RingEquiv.{u, v}
      (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
      S),
    f =
      e.toRingHom.comp
        (algebraMap R
          (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) :
            Type u))

Tactic:
obtain ⟨T, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R S

Premises used: Algebra.FiniteType.exists_fgAlgCatSkeleton
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
T : FGAlgCatSkeleton R
e :
  S ≃ₐ[R]
    (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
⊢ ∃ (T : FGAlgCatSkeleton R) (e :
    RingEquiv.{u, v}
      (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
      S),
    f =
      e.toRingHom.comp
        (algebraMap R
          (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) :
            Type u))

Tactic:
⟨T, e.symm.toRingEquiv, e.symm.toAlgHom.comp_algebraMap.symm⟩

Premises used: AlgHom.comp_algebraMap, AlgEquiv.toAlgHom, AlgEquiv.symm, AlgEquiv.toRingEquiv, Exists.intro, Eq.symm
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FiniteType R S
T : FGAlgCatSkeleton R
e :
  S ≃ₐ[R]
    (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
⊢ ∃ (T : FGAlgCatSkeleton R) (e :
    RingEquiv.{u, v}
      (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) : Type u)
      S),
    f =
      e.toRingHom.comp
        (algebraMap R
          (↑((FGAlgCatSkeleton.eval R T).obj (P := fun (A : CommAlgCat R) ↦ Algebra.FiniteType R (↑A : Type u))) :
            Type u))

Tactic:
exact ⟨T, e.symm.toRingEquiv, e.symm.toAlgHom.comp_algebraMap.symm⟩
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
⊢ Functor.Full (C := FGAlgCat.{u_1, u} R) (FGAlgCat.uliftFunctor.{u_2, u_1, u} R)

Tactic:
(FGAlgCat.fullyFaithfulUliftFunctor R).full

Premises used: FGAlgCat.fullyFaithfulUliftFunctor, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
⊢ Functor.Faithful (C := FGAlgCat.{u_1, u} R) (FGAlgCat.uliftFunctor.{u_2, u_1, u} R)

Tactic:
(FGAlgCat.fullyFaithfulUliftFunctor R).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, FGAlgCat.fullyFaithfulUliftFunctor
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
Q : MorphismProperty CommRingCat
hQ : Q ≤ toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ FiniteType
R : CommRingCat
⊢ EssentiallySmall.{u, u, u + 1} (Q.Under ⊤ R)

Tactic:
essentiallySmall_of_fully_faithful
    (MorphismProperty.Comma.changeProp _ _ hQ
      le_rfl le_rfl ⋙ (FGAlgCat.equivUnder R).inverse)

Premises used: le_rfl, CategoryTheory.Functor.comp, CategoryTheory.essentiallySmall_of_fully_faithful, FGAlgCat.equivUnder, CategoryTheory.MorphismProperty.Comma.changeProp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ (A.binaryCofan B).inl = ofHom includeLeft

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ (A.binaryCofan B).inr = ofHom includeRight

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ (A.binaryCofan B).pt = of R ((↑A : Type u) ⊗[R] (↑B : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
hf :
  Hom.hom
      ((A.binaryCofan B).inl ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom f
⊢ (A.binaryCofan B).inl ≫
      (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g =
    f

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ Hom.hom
      ((A.binaryCofan B).inl ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom f

Tactic:
lift_comp_includeLeft _ _ fun _ _ ↦ .all _ _

Premises used: Algebra.TensorProduct.lift_comp_includeLeft, Algebra.TensorProduct.includeLeft, Quotient, TensorProduct, AddCon.Quotient, AlgHom.comp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ Hom.hom
      ((A.binaryCofan B).inl ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom f

Tactic:
exact lift_comp_includeLeft _ _ fun _ _ ↦ .all _ _

Premises used: Algebra.TensorProduct.lift_comp_includeLeft
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
hf :
  Hom.hom
      ((A.binaryCofan B).inr ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom g
⊢ (A.binaryCofan B).inr ≫
      (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g =
    g

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ Hom.hom
      ((A.binaryCofan B).inr ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom g

Tactic:
lift_comp_includeRight _ _ fun _ _ ↦ .all _ _

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.TensorProduct.lift_comp_includeRight, MonoidHomClass.toMonoidHom, Quotient, RingHomClass.toRingHom, TensorProduct, AddCon.Quotient, AlgHom.comp, Algebra.TensorProduct.includeRight
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ Hom.hom
      ((A.binaryCofan B).inr ≫
        (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
            (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
              Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
          f g) =
    Hom.hom g

Tactic:
exact lift_comp_includeRight _ _ fun _ _ ↦ .all _ _

Premises used: Algebra.TensorProduct.lift_comp_includeRight
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
hf :
  Hom.hom m =
    Hom.hom
      ((fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g)
⊢ m =
    (fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
        (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
          Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
      f g

Tactic:
ext1
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Hom.hom m =
    Hom.hom
      ((fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g)

Tactic:
liftEquiv.symm_apply_eq (y := ⟨⟨_, _⟩, fun _ _ ↦ .all _ _⟩).mp ?_

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, Equiv.symm_apply_eq, Quotient, Iff.mp, TensorProduct, Algebra.TensorProduct.liftEquiv, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
hf :
  Eq (α :=
    { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (((Equiv.symm Algebra.TensorProduct.liftEquiv :
            ((↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) ≃
              { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
                ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                  Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
                    ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) }) :
          (a : (↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) →
            { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
              ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                Commute ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x)
                  ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y) })
        (Hom.hom m) :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (Subtype.mk (p := fun (fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u))) ↦
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)))
        (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            f,
          ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            g)
        ⋯ :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
⊢ Hom.hom m =
    Hom.hom
      ((fun {T : CommAlgCat R} (f : A ⟶ T) (g : B ⟶ T) ↦
          (ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯) :
            Quiver.Hom (V := CommAlgCat R) (of R ((↑A : Type u) ⊗[R] (↑B : Type u))) (of R (↑T : Type u))))
        f g)

Tactic:
refine liftEquiv.symm_apply_eq (y := ⟨⟨_, _⟩, fun _ _ ↦ .all _ _⟩).mp ?_

Premises used: Equiv.symm_apply_eq, Iff.mp, Algebra.TensorProduct.liftEquiv
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Eq (α :=
    { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (((Equiv.symm Algebra.TensorProduct.liftEquiv :
            ((↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) ≃
              { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
                ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                  Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
                    ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) }) :
          (a : (↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) →
            { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
              ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                Commute ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x)
                  ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y) })
        (Hom.hom m) :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (Subtype.mk (p := fun (fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u))) ↦
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)))
        (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            f,
          ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            g)
        ⋯ :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })

Tactic:
Subtype.ext (Prod.ext congr(($hm₁).hom) congr(($hm₂).hom))

Premises used: congrArg, id, Prod.ext, CommAlgCat.Hom.hom, Subtype.ext
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
m : (A.binaryCofan B).pt ⟶ T
hm₁ : (A.binaryCofan B).inl ≫ m = f
hm₂ : (A.binaryCofan B).inr ≫ m = g
⊢ Eq (α :=
    { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
      ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
        Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
          ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (((Equiv.symm Algebra.TensorProduct.liftEquiv :
            ((↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) ≃
              { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
                ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                  Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
                    ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) }) :
          (a : (↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑T : Type u)) →
            { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
              ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
                Commute ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x)
                  ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y) })
        (Hom.hom m) :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })
    (Subtype.mk (p := fun (fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u))) ↦
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)))
        (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            f,
          ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)
            g)
        ⋯ :
      { fg : ((↑A : Type u) →ₐ[R] (↑T : Type u)) × ((↑B : Type u) →ₐ[R] (↑T : Type u)) //
        ∀ (x : (↑A : Type u)) (y : (↑B : Type u)),
          Commute (S := (↑T : Type u)) ((fg.1 : (a : (↑A : Type u)) → (↑T : Type u)) x : (↑T : Type u))
            ((fg.2 : (a : (↑B : Type u)) → (↑T : Type u)) y : (↑T : Type u)) })

Tactic:
exact Subtype.ext (Prod.ext congr(($hm₁).hom) congr(($hm₂).hom))
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
⊢ (↑((𝟙_ (CommAlgCat R)) (𝒞 := instCategory)) : Type u) = R

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ (↑(tensorObj (𝒞 := instCategory) A B) : Type u) = (↑A : Type u) ⊗[R] (↑B : Type u)

Tactic:
rfl

Premises used: Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
f : A ⟶ C
g : B ⟶ D
⊢ Hom.hom (f ⊗ₘ g) = Algebra.TensorProduct.map (Hom.hom f) (Hom.hom g)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat R
f : A ⟶ B
⊢ Hom.hom (f ▷ C) = Algebra.TensorProduct.map (Hom.hom f) (AlgHom.id R (↑C : Type u))

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat R
f : A ⟶ B
⊢ Hom.hom (C ◁ f) = Algebra.TensorProduct.map (AlgHom.id R (↑C : Type u)) (Hom.hom f)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat R
⊢ Hom.hom (Iso.hom (α_ A B C)) =
    (↑(assoc R R R (↑A : Type u) (↑B : Type u) (↑C : Type u)) :
      (↑A : Type u) ⊗[R] (↑B : Type u) ⊗[R] (↑C : Type u) →ₐ[R] (↑A : Type u) ⊗[R] ((↑B : Type u) ⊗[R] (↑C : Type u)))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat R
⊢ Hom.hom (Iso.inv (α_ A B C)) =
    (↑(AlgEquiv.symm (assoc R R R (↑A : Type u) (↑B : Type u) (↑C : Type u))) :
      (↑A : Type u) ⊗[R] ((↑B : Type u) ⊗[R] (↑C : Type u)) →ₐ[R] (↑A : Type u) ⊗[R] (↑B : Type u) ⊗[R] (↑C : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, Quotient, TensorProduct, AddCon.Quotient, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ Hom.hom (Iso.hom (β_ A B)) =
    (↑(Algebra.TensorProduct.comm R (↑A : Type u) (↑B : Type u)) :
      (↑A : Type u) ⊗[R] (↑B : Type u) →ₐ[R] (↑B : Type u) ⊗[R] (↑A : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat R
⊢ Hom.hom (Iso.inv (β_ A B)) =
    (↑(Algebra.TensorProduct.comm R (↑B : Type u) (↑A : Type u)) :
      (↑B : Type u) ⊗[R] (↑A : Type u) →ₐ[R] (↑A : Type u) ⊗[R] (↑B : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl