awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Coalgebra R M
inst_6 : Coalgebra R N
simp :
  Eq (α := (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R] R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom (ε ⊗ₘ ε) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)
⊢ Eq.{u + 1} (α := (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R] R)
    (ModuleCat.Hom.hom ε :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    CoalgebraStruct.counit

Tactic:
simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]

Premises used: TensorProduct.AlgebraTensorModule.rid_eq_rid, TensorProduct.counit_def, TensorProduct.lid_eq_rid
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : Coalgebra R M
inst_6 : Coalgebra R N
⊢ Eq (α := (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R] R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom (ε ⊗ₘ ε) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
simp :
  Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom (ε ⊗ₘ (ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.counit
        ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
          AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit))
⊢ Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom ε :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    CoalgebraStruct.counit

Tactic:
simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]

Premises used: TensorProduct.AlgebraTensorModule.rid_eq_rid, TensorProduct.counit_def, TensorProduct.lid_eq_rid
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
⊢ Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom (ε ⊗ₘ (ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.counit
        ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
          AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
simp :
  Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R))) ⊗ₘ ε) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map
        ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
          AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)
        CoalgebraStruct.counit)
⊢ Eq.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom ε :
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    CoalgebraStruct.counit

Tactic:
simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]

Premises used: TensorProduct.AlgebraTensorModule.rid_eq_rid, TensorProduct.counit_def, TensorProduct.lid_eq_rid
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Goal:
R : Type u
inst : CommRing R
M N P : Type u
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
inst_7 : Coalgebra R M
inst_8 : Coalgebra R N
inst_9 : Coalgebra R P
⊢ Eq (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      R)
    (ModuleCat.Hom.hom (Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)))) ∘ₗ
        ModuleCat.Hom.hom ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R))) ⊗ₘ ε) :
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
        (↑((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) : Type u))
    ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
      AlgebraTensorModule.map
        ((↑(TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ
          AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)
        CoalgebraStruct.counit)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : CommAlgCat.{v, u} R
⊢ Hom.hom (𝟙 A) = AlgHom.id R (↑A : Type v)

Tactic:
rfl

Premises used: AlgHom.id, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : CommAlgCat.{v, u} R
a : (↑A : Type v)
⊢ (@ConcreteCategory.hom _ instCategory (fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
          carrier
          (fun (X Y : CommAlgCat.{v, u} R) ↦
            (AlgHom.funLike : FunLike ((↑X : Type v) →ₐ[R] (↑Y : Type v)) (↑X : Type v) (↑Y : Type v)))
          _ _ _ (𝟙 A : A ⟶ A) :
        (a : (↑A : Type v)) → (↑A : Type v))
      a =
    a

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: AlgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
a : (↑A : Type v)
⊢ Eq (α := (↑C : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
            carrier) (f ≫ g) :
          (a : (↑A : Type v)) → (↑C : Type v))
        a :
      (↑C : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑B : Type v)) → (↑C : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
                carrier) f :
              (a : (↑A : Type v)) → (↑B : Type v))
            a :
          (↑B : Type v)) :
      (↑C : Type v))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
f g : A ⟶ B
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: CommAlgCat.Hom.ext
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
f : X →ₐ[R] Y
⊢ Hom.hom (ofHom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
f : A ⟶ B
⊢ ofHom (Hom.hom f) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
⊢ Eq (α := Quiver.Hom (V := CommAlgCat.{v, u} R) (of R X) (of R X)) (ofHom (AlgHom.id R X)) (𝟙 (of R X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
inst_5 : CommRing Z
inst_6 : Algebra R Z
f : X →ₐ[R] Y
g : Y →ₐ[R] Z
⊢ ofHom (g.comp f) = ofHom f ≫ ofHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
f : X →ₐ[R] Y
x : X
⊢ Eq (α := (↑(of R Y) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
            carrier) (ofHom f) :
          (a : (↑(of R X) : Type v)) → (↑(of R Y) : Type v))
        x :
      (↑(of R Y) : Type v))
    ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
e : A ≅ B
x : (↑A : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          e.inv :
        (a : (↑B : Type v)) → (↑A : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier) e.hom :
            (a : (↑A : Type v)) → (↑B : Type v))
          x :
        (↑B : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
e : A ≅ B
x : (↑B : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          e.hom :
        (a : (↑A : Type v)) → (↑B : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier) e.inv :
            (a : (↑B : Type v)) → (↑A : Type v))
          x :
        (↑A : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : CommAlgCat.{v, u} R
⊢ Functor.obj
      (forget (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CC := carrier))
      A =
    (↑A : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
f : A ⟶ B
⊢ Eq (α :=
    (a :
        (fun (X : Type v) ↦ X)
          (Functor.obj
            (forget (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦
              (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier))
            A)) →
      (fun (X : Type v) ↦ X)
        (Functor.obj
          (forget (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
            (CC := carrier))
          B))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦
              (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier))
            f)) :
      (a : (fun (X : Type v) ↦ X) ((forget (CommAlgCat R)).obj A)) →
        (fun (X : Type v) ↦ X) ((forget (CommAlgCat R)).obj B))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
          carrier) f) :
      (a : (↑A : Type v)) → (↑B : Type v))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : CommAlgCat.{v, u} R
⊢ Functor.obj
      (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CC := carrier) CommRingCat (FD := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CD :=
        CommRingCat.carrier))
      A =
    CommRingCat.of (↑A : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
f : A ⟶ B
⊢ Eq (α :=
    Functor.obj
        (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
          (CC := carrier) CommRingCat (FD := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CD :=
          CommRingCat.carrier))
        A ⟶
      Functor.obj
        (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
          (CC := carrier) CommRingCat (FD := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CD :=
          CommRingCat.carrier))
        B)
    (CategoryTheory.Functor.map
      (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CC := carrier) CommRingCat (FD := fun (R S : CommRingCat.{v}) ↦ (↑R : Type v) →+* (↑S : Type v)) (CD :=
        CommRingCat.carrier))
      f)
    (CommRingCat.ofHom (↑(Hom.hom f) : (↑A : Type v) →+* (↑B : Type v)))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A : CommAlgCat.{v, u} R
⊢ Functor.obj
      (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CC := carrier) (AlgCat.{v, u} R) (FD := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CD := AlgCat.carrier))
      A =
    AlgCat.of R (↑A : Type v)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B : CommAlgCat.{v, u} R
f : A ⟶ B
⊢ CategoryTheory.Functor.map
      (forget₂ (CommAlgCat.{v, u} R) (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CC := carrier) (AlgCat.{v, u} R) (FD := fun (x1 x2 : AlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v))
        (CD := AlgCat.carrier))
      f =
    AlgCat.ofHom (Hom.hom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
inst_5 : CommRing Z
inst_6 : Algebra R Z
i : A ≅ B
x : (↑A : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          i.inv :
        (a : (↑B : Type v)) → (↑A : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier) i.hom :
            (a : (↑A : Type v)) → (↑B : Type v))
          x :
        (↑B : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
inst_5 : CommRing Z
inst_6 : Algebra R Z
i : A ≅ B
x : (↑B : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC := carrier)
          i.hom :
        (a : (↑A : Type v)) → (↑B : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommAlgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐ[R] (↑x2 : Type v)) (CC :=
              carrier) i.inv :
            (a : (↑B : Type v)) → (↑A : Type v))
          x :
        (↑A : Type v)) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X_1 Y_1 Z : Type v
inst_1 : CommRing X_1
inst_2 : Algebra R X_1
inst_3 : CommRing Y_1
inst_4 : Algebra R Y_1
inst_5 : CommRing Z
inst_6 : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      f)
i : Functor.obj
    (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      f)
e : (↑X : Type u) ≃ₐ[R] (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑(↑__src.toRingHom : (↑X : Type u) →* (↑Y : Type u)) : OneHom (↑X : Type u) (↑Y : Type u)).toFun,
    invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f

Tactic:
(isoMk e).isIso_hom

Premises used: AlgEquiv.toAlgHom, CategoryTheory.Iso.isIso_hom, CommAlgCat.isoMk
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X_1 Y_1 Z : Type v
inst_1 : CommRing X_1
inst_2 : Algebra R X_1
inst_3 : CommRing Y_1
inst_4 : Algebra R Y_1
inst_5 : CommRing Z
inst_6 : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      f)
i : Functor.obj
    (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier)) X ≅
  Functor.obj
    (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (CommAlgCat R) (FC := fun (x1 x2 : CommAlgCat R) ↦ (↑x1 : Type u) →ₐ[R] (↑x2 : Type u)) (CC := carrier))
      f)
e : (↑X : Type u) ≃ₐ[R] (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑(↑__src.toRingHom : (↑X : Type u) →* (↑Y : Type u)) : OneHom (↑X : Type u) (↑Y : Type u)).toFun,
    invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f

Tactic:
exact (isoMk e).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CommAlgCat.isoMk
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
inst_5 : CommRing Z
inst_6 : Algebra R Z
⊢ Functor.Full (C := CommAlgCat.{u_1, u} R) (uliftFunctor.{u_2, u_1, u} R)

Tactic:
(fullyFaithfulUliftFunctor R).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CommAlgCat.fullyFaithfulUliftFunctor
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
A B C : CommAlgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Algebra R X
inst_3 : CommRing Y
inst_4 : Algebra R Y
inst_5 : CommRing Z
inst_6 : Algebra R Z
⊢ Functor.Faithful (C := CommAlgCat.{u_1, u} R) (uliftFunctor.{u_2, u_1, u} R)

Tactic:
(fullyFaithfulUliftFunctor R).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CommAlgCat.fullyFaithfulUliftFunctor
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
⊢ HasColimits.{u, u + 1} (CommAlgCat R)

Tactic:
Adjunction.has_colimits_of_equivalence (commAlgCatEquivUnder (.of R)).functor

Premises used: CategoryTheory.Equivalence.functor, CommRingCat.of, CategoryTheory.Adjunction.has_colimits_of_equivalence, commAlgCatEquivUnder
-- Module: Mathlib.Algebra.Category.CommAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
⊢ HasLimits.{u, u + 1} (CommAlgCat R)

Tactic:
Adjunction.has_limits_of_equivalence (commAlgCatEquivUnder (.of R)).functor

Premises used: CategoryTheory.Adjunction.has_limits_of_equivalence, CategoryTheory.Equivalence.functor, CommRingCat.of, commAlgCatEquivUnder
-- Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType
Goal:
R : Type u
inst : CommRing R
A : FGAlgCat.{u_1, u} R
⊢ Algebra.FiniteType.{u, u_1} R
    (↑(A.obj (P := fun (A : CommAlgCat.{u_1, u} R) ↦ Algebra.FiniteType.{u, u_1} R (↑A : Type u_1))) : Type u_1)

Tactic:
A.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- 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
obtain :
  ∀ (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))
⊢ ∃ (P : FGAlgCatSkeleton R),
    Nonempty
      (A ≃ₐ[R] (↑((FGAlgCatSkeleton.eval R P).obj (P := fun (A : CommAlgCat R) ↦ FiniteType R (↑A : Type u))) : Type u))

Tactic:
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h

Premises used: Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''