awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.AlgCat.Limits (goal)
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
⊢ EquivLike.coe (E :=
      (↑(F ⋙
                forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier)).sections :
          Type (max w v)) ≃
        Shrink.{w, max w v}
          (↑(F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier)).sections :
            Type (max w v)))
      (equivShrink
        (↑(F ⋙
                forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier)).sections :
          Type (max w v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).obj
                j) ↦
        x ∈
          (F ⋙
              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                (CC := carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                      s))
                  j) :
              (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
                (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
            1)
        ⋯) =
    1
have refine_1 : Eq (α :=
  (j : J) →
    (F ⋙
          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
            carrier)).obj
      j)
  (fun (j : J) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Cone.π
              (Functor.mapCone
                (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier))
                s))
            j) :
        (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
          (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
      1)
  1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Category.AlgCat.Limits (goal)
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
⊢ Eq (α :=
    (j : J) →
      (F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).obj
        j)
    (fun (j : J) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cone.π
                (Functor.mapCone
                  (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))
                  s))
              j) :
          (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        1)
    1
have refine_1 : ∀ (j : J),
  Eq (α :=
    (fun (X : Type w) ↦ X)
      ((F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).obj
        j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cone.π
                (Functor.mapCone
                  (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))
                  s))
              j) :
          (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        1 :
      (fun (X : Type w) ↦ X)
        ((F ⋙
              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                (CC := carrier)).obj
          j))
    (1 j : (↑(F.obj j) : Type w))
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Category.BoolRing (goal)
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
⊢ { hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) : α.Hom β } ≫
      { hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) } =
    𝟙 α
have hf : ∀ (x : (↑α : Type u)),
  Eq (α := (↑α : Type u))
    ((Hom.hom
            ({ hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) : α.Hom β } ≫
              { hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) }) :
          (a : (↑α : Type u)) → (↑α : Type u))
        x :
      (↑α : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α : Type u)) → (↑α : Type u)) x : (↑α : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.BoolRing (goal)
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
⊢ { hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) : β.Hom α } ≫
      { hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) } =
    𝟙 β
have hf : ∀ (x : (↑β : Type u)),
  Eq (α := (↑β : Type u))
    ((Hom.hom
            ({ hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) : β.Hom α } ≫
              { hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) }) :
          (a : (↑β : Type u)) → (↑β : Type u))
        x :
      (↑β : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β : Type u)) → (↑β : Type u)) x : (↑β : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
Goal:
R : Type u
inst : CommRing R
X : CoalgCat R
⊢ Eq (α :=
    (↑(ModuleCat.of R (↑X.toModuleCat : Type u)) : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
            (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑X.toModuleCat : Type u)))) :
        Type u))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑X.toModuleCat : Type u)))
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.of R (↑X.toModuleCat : Type u) ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑X.toModuleCat : Type u)))
        (ModuleCat.ofHom CoalgebraStruct.comul)
        (ModuleCat.ofHom CoalgebraStruct.comul ▷ ModuleCat.of R (↑X.toModuleCat : Type u) ≫
          Iso.hom
            (α_ (ModuleCat.of R (↑X.toModuleCat : Type u)) (ModuleCat.of R (↑X.toModuleCat : Type u))
              (ModuleCat.of R (↑X.toModuleCat : Type u))))))
have simp_rw : Eq (α :=
  (↑X.toModuleCat : Type u) →ₗ[R]
    (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)) :
      Type u))
  (ModuleCat.Hom.hom
    (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
      (ModuleCat.ofHom CoalgebraStruct.comul) (X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul)))
  (ModuleCat.Hom.hom
    (CategoryStruct.comp (Y := tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat X.toModuleCat)
      (ModuleCat.ofHom CoalgebraStruct.comul)
      (ModuleCat.ofHom CoalgebraStruct.comul ▷ X.toModuleCat ≫ Iso.hom (α_ X.toModuleCat X.toModuleCat X.toModuleCat))))
Tactic: simp_rw [ModuleCat.of_coe]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
Goal:
R : Type u
inst : CommRing R
K L : CoalgCat R
⊢ Eq.{u + 1} (α :=
    (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
      TensorProduct R (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u)
        (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (tensorObj (𝒞 := category) K L).toModuleCat
              (tensorObj (𝒞 := category) K L).toModuleCat) :
          Type u))
    ((↑(TensorProduct.tensorTensorTensorComm R (↑K.toModuleCat : Type u) (↑K.toModuleCat : Type u)
            (↑L.toModuleCat : Type u) (↑L.toModuleCat : Type u)) :
        TensorProduct R (TensorProduct R (↑K.toModuleCat : Type u) (↑K.toModuleCat : Type u))
            (TensorProduct R (↑L.toModuleCat : Type u) (↑L.toModuleCat : Type u)) →ₗ[R]
          TensorProduct R (TensorProduct R (↑K.toModuleCat : Type u) (↑L.toModuleCat : Type u))
            (TensorProduct R (↑K.toModuleCat : Type u) (↑L.toModuleCat : Type u))) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul)
have simp : Eq.{u + 1} (α :=
  (↑(tensorObj (𝒞 := category) K L).toModuleCat : Type u) →ₗ[R]
    (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (tensorObj (𝒞 := ModuleCat.moduleCategory R) K.toModuleCat K.toModuleCat)
          (tensorObj (𝒞 := ModuleCat.moduleCategory R) L.toModuleCat L.toModuleCat)) :
      Type u))
  (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
  (TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul)
Tactic: simp only [Comon.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse,
    comonEquivalence_functor, toComon_obj, toComonObj_X, ModuleCat.of_coe,
    MonObj.tensorObj.mul_def, unop_comp, unop_tensorObj, unop_tensorHom,
    BraidedCategory.unop_tensorμ, tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp,
    ModuleCat.hom_ofHom, LinearEquiv.comp_toLinearMap_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R) (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N)))
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N)))) :
          Type u))
    CoalgebraStruct.comul
have simp : Eq.{u + 1} (α :=
  (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))) : Type u) →ₗ[R]
    (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R M) (ModuleCat.of R M))
          (tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R N) (ModuleCat.of R N))) :
      Type u))
  (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul))
  (AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)
Tactic: simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
    AlgebraTensorModule.tensorTensorTensorComm_eq]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))
              (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))) :
          Type u))
    CoalgebraStruct.comul
have simp : Eq.{u + 1} (α :=
  (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) ⊗[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u))
  (ModuleCat.Hom.hom (Quiver.Hom.unop MonObj.mul) :
    (↑(toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P)))) : Type u) →ₗ[R]
      (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))
            (toModuleCat (tensorObj (𝒞 := category) (of R M) (tensorObj (𝒞 := category) (of R N) (of R P))))) :
        Type u))
  CoalgebraStruct.comul
Tactic: simp only [Comon.monoidal_tensorObj_comon_comul]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{u + 1} (α :=
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) ⊗[R]
        (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u))
    (ModuleCat.Hom.hom Δ :
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
        (↑(tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P)))
              (toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P)))) :
          Type u))
    CoalgebraStruct.comul
have dsimp : Eq (α :=
  (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) →ₗ[R]
    (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u) ⊗[R]
      (↑(toModuleCat (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (of R M) (of R N)) (of R P))) : Type u))
  (ModuleCat.Hom.hom
      (Quiver.Hom.unop
        (tensorμ (Opposite.op (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))))
          (Opposite.op (ModuleCat.of R P)) (Opposite.op (toModuleCat (tensorObj (𝒞 := category) (of R M) (of R N))))
          (Opposite.op (ModuleCat.of R P)))) ∘ₗ
    ModuleCat.Hom.hom
      ((Quiver.Hom.unop MonObj.mul ⊗ₘ Quiver.Hom.unop MonObj.mul) ≫
          Quiver.Hom.unop
            (tensorμ (Opposite.op (ModuleCat.of R M)) (Opposite.op (ModuleCat.of R N)) (Opposite.op (ModuleCat.of R M))
              (Opposite.op (ModuleCat.of R N))) ⊗ₘ
        Quiver.Hom.unop MonObj.mul))
  CoalgebraStruct.comul
Tactic: dsimp +instances
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{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
have 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)
Tactic: simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{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
have 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))
Tactic: simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.ComonEquivalence (goal)
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.{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
have 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)
Tactic: simp [TensorProduct.counit_def, TensorProduct.AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.FiniteType (goal)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : CommRing A
inst_2 : Algebra R A
h : FiniteType 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))
have 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))
Tactic: obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp h
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.FiniteType (hypothesis)
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
f : R →+* S
hf : f.FiniteType
⊢ ∃ (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))
have algebraizeInst : Algebra.FiniteType R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.FiniteType (goal)
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 :
    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))
have 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))
Tactic: obtain ⟨T, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R S
-- Lean 4 proof step from Mathlib.Algebra.Category.CommAlgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
A B C D T : CommAlgCat R
f : A ⟶ T
g : B ⟶ T
⊢ (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
have 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) sorry) :
            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: ext1