awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B C : CommBialgCat.{v, u} R
X_1 Y_1 Z : Type v
inst_1 : CommRing X_1
inst_2 : Bialgebra R X_1
inst_3 : CommRing Y_1
inst_4 : Bialgebra R Y_1
inst_5 : CommRing Z
inst_6 : Bialgebra R Z
X Y : CommBialgCat R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (CommBialgCat R) (FC := fun (x1 x2 : CommBialgCat R) ↦ (↑x1 : Type u) →ₐc[R] (↑x2 : Type u)) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (CommBialgCat R) (FC := fun (x1 x2 : CommBialgCat R) ↦ (↑x1 : Type u) →ₐc[R] (↑x2 : Type u)) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget (CommBialgCat R) (FC := fun (x1 x2 : CommBialgCat R) ↦ (↑x1 : Type u) →ₐc[R] (↑x2 : Type u)) (CC :=
      carrier))
    X ≅
  Functor.obj
    (forget (CommBialgCat R) (FC := fun (x1 x2 : CommBialgCat R) ↦ (↑x1 : Type u) →ₐc[R] (↑x2 : Type u)) (CC :=
      carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (CommBialgCat R) (FC := fun (x1 x2 : CommBialgCat R) ↦ (↑x1 : Type u) →ₐc[R] (↑x2 : Type u)) (CC :=
        carrier))
      f)
e : (↑X : Type u) ≃ₐc[R] (↑Y : Type u) :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact (isoMk e).isIso_hom

Premises used: CommBialgCat.isoMk, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
a :
  ∀ (x : (↑(unop (op (of R A))) : Type u)),
    Eq (α :=
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))
      ((Hom.hom
              (Quiver.Hom.unop
                (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
                ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)) (op (of R A)))) :
          Type u))
      ((Hom.hom (Quiver.Hom.unop (Iso.hom (λ_ (op (of R A))))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
                ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)) (op (of R A)))) :
          Type u))
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
        (op (of R A)))
      (op (of R A)))
    (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (λ_ (op (of R A))))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
            (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (λ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))

Tactic:
Coalgebra.rTensor_counit_comul _

Premises used: Quotient.liftOn', AddCon.liftOn, Quotient, Coalgebra.rTensor_counit_comul, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
            (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (counitAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (λ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (𝟙_ (CommAlgCat R)ᵒᵖ ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))
              (op (of R A)))) :
        Type u))

Tactic:
exact Coalgebra.rTensor_counit_comul _

Premises used: Coalgebra.rTensor_counit_comul
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
a :
  ∀ (x : (↑(unop (op (of R A))) : Type u)),
    Eq (α :=
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))
      ((Hom.hom
              (Quiver.Hom.unop
                (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
                ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
          Type u))
      ((Hom.hom (Quiver.Hom.unop (Iso.hom (ρ_ (op (of R A))))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
                ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
          Type u))
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
        ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))
      (op (of R A)))
    (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (ρ_ (op (of R A))))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
            ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (ρ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))

Tactic:
Coalgebra.lTensor_counit_comul _

Premises used: Coalgebra.lTensor_counit_comul, Quotient.liftOn', AddCon.liftOn, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, AddCon.toQuotient
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
            ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (op (of R A) ◁ Quiver.Hom.op (ofHom (counitAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))
    ((Hom.hom (Quiver.Hom.unop (Iso.hom (ρ_ (op (of R A))))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop (op (of R A) ⊗ 𝟙_ (CommAlgCat R)ᵒᵖ)) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A))
              ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite)))) :
        Type u))

Tactic:
exact Coalgebra.lTensor_counit_comul _

Premises used: Coalgebra.lTensor_counit_comul
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
a :
  ∀ (x : (↑(unop (op (of R A))) : Type u)),
    Eq (α :=
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))
      ((Hom.hom
              (Quiver.Hom.unop
                (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
                (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A)))
                (op (of R A)))) :
          Type u))
      ((Hom.hom
              (Quiver.Hom.unop
                (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
                  op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
            (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
                (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A)))
                (op (of R A)))) :
          Type u))
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
        (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))
      (op (of R A)))
    (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))
    (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
      op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
                op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))

Tactic:
(Coalgebra.coassoc_symm_apply _).symm

Premises used: Coalgebra.coassoc_symm_apply, Quotient.liftOn', AddCon.liftOn, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, Eq.symm, AddCon.toQuotient
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
x : (↑(unop (op (of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
      Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Quiver.Hom.op (ofHom (comulAlgHom R A)) ▷ op (of R A) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))
    ((Hom.hom
            (Quiver.Hom.unop
              (Iso.hom (α_ (op (of R A)) (op (of R A)) (op (of R A))) ≫
                op (of R A) ◁ Quiver.Hom.op (ofHom (comulAlgHom R A)) ≫ Quiver.Hom.op (ofHom (comulAlgHom R A)))) :
          (a : (↑(unop (op (of R A))) : Type u)) → (↑(unop ((op (of R A) ⊗ op (of R A)) ⊗ op (of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite)
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A))) (op (of R A)))) :
        Type u))

Tactic:
exact (Coalgebra.coassoc_symm_apply _).symm

Premises used: Coalgebra.coassoc_symm_apply, Eq.symm
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
⊢ Eq.{u + 1} (α :=
    (↑(unop (op (of R A))) : Type u) →ₐ[R] (↑(unop ((𝟙_ (CommAlgCat R)ᵒᵖ) (𝒞 := Category.opposite))) : Type u))
    (Hom.hom (Quiver.Hom.unop η)) (counitAlgHom R A)

Tactic:
rfl

Premises used: AlgHom.ofLinearMap, Bialgebra.counitAlgHom, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
⊢ Eq.{u + 1} (α :=
    (↑(unop (op (of R A))) : Type u) →ₐ[R]
      (↑(unop (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (of R A)) (op (of R A)))) : Type u))
    (Hom.hom (Quiver.Hom.unop μ)) (comulAlgHom R A)

Tactic:
rfl

Premises used: Bialgebra.comulAlgHom, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
a :
  ∀ (x : (↑(unop (op (CommAlgCat.of R A))) : Type u)),
    Eq (α :=
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))
      ((CommAlgCat.Hom.hom (Quiver.Hom.unop (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ)) :
            (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
              (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
                (op (CommAlgCat.of R A)))) :
          Type u))
      ((CommAlgCat.Hom.hom (Quiver.Hom.unop μ) :
            (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
              (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
          x :
        (↑(unop
              (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
                (op (CommAlgCat.of R A)))) :
          Type u))
⊢ Eq (α :=
    Quiver.Hom (V := (CommAlgCat R)ᵒᵖ)
      (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A)))
      (op (CommAlgCat.of R A)))
    (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ) μ

Tactic:
ext
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
x : (↑(unop (op (CommAlgCat.of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
            (op (CommAlgCat.of R A)))) :
      Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ)) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop μ) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))

Tactic:
comm_comul R _

Premises used: Quotient.liftOn', AddCon.liftOn, Coalgebra.comm_comul, Quotient, TensorProduct, AddCon.Quotient
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Bialgebra R A
inst_3 : IsCocomm R A
x : (↑(unop (op (CommAlgCat.of R A))) : Type u)
⊢ Eq (α :=
    (↑(unop
          (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
            (op (CommAlgCat.of R A)))) :
      Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop (Iso.hom (β_ (op (CommAlgCat.of R A)) (op (CommAlgCat.of R A))) ≫ μ)) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))
    ((CommAlgCat.Hom.hom (Quiver.Hom.unop μ) :
          (a : (↑(unop (op (CommAlgCat.of R A))) : Type u)) →
            (↑(unop (op (CommAlgCat.of R A) ⊗ op (CommAlgCat.of R A))) : Type u))
        x :
      (↑(unop
            (MonoidalCategoryStruct.tensorObj (𝒞 := Category.opposite) (op (CommAlgCat.of R A))
              (op (CommAlgCat.of R A)))) :
        Type u))

Tactic:
exact comm_comul R _

Premises used: Coalgebra.comm_comul
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B : CommBialgCat R
f : A ⟶ B
⊢ Mon.Hom.hom
      (Quiver.Hom.unop (CategoryTheory.Functor.map (Equivalence.functor (commBialgCatEquivComonCommAlgCat R)) f)) =
    (CommAlgCat.ofHom (↑(CommBialgCat.Hom.hom f) : (↑A : Type u) →ₐ[R] (↑B : Type u))).op

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B : (Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ
f : A ⟶ B
⊢ (↑(CommBialgCat.Hom.hom (CategoryTheory.Functor.map (Equivalence.inverse (commBialgCatEquivComonCommAlgCat R)) f)) :
      (↑((commBialgCatEquivComonCommAlgCat R).inverse.obj A) : Type u) →ₐ[R]
        (↑((commBialgCatEquivComonCommAlgCat R).inverse.obj B) : Type u)) =
    CommAlgCat.Hom.hom f.unop.hom.unop

Tactic:
rfl

Premises used: BialgHom.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : CommBialgCat R
inst_1 : IsCocomm R (↑A : Type u)
⊢ IsCommMonObj (unop (Functor.obj (Equivalence.functor (commBialgCatEquivComonCommAlgCat R)) A)).X

Tactic:
inferInstanceAs <| IsCommMonObj <| op <| CommAlgCat.of R A

Premises used: _private.0.instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier._proof_1
-- Module: Mathlib.Algebra.Category.ContinuousCohomology.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : Group G
inst_2 : TopologicalSpace R
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
rep : Action (TopModuleCat.{u_3, u_1} R) G
g : G
x x_1 : ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)
h :
  ∀ (a : G),
    Eq.{u_3 + 1} (α := (↑rep.V.toModuleCat : Type u_3))
      (((ContinuousMap.comp
                (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
                  C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                ((x + x_1).comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))) :
              ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3)) :
            (a : G) → (↑rep.V.toModuleCat : Type u_3))
          a :
        (↑rep.V.toModuleCat : Type u_3))
      ((HAdd.hAdd (α := ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3))
              (ContinuousMap.comp
                (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
                  C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                (x.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))))
              (ContinuousMap.comp
                (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
                  C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
                (x_1.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G)))) :
            (a : G) → (↑rep.V.toModuleCat : Type u_3))
          a :
        (↑rep.V.toModuleCat : Type u_3))
⊢ ContinuousMap.comp
      (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
        C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
      ((x + x_1).comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))) =
    HAdd.hAdd (α := ContinuousMap.{u_2, u_3} G (↑rep.V.toModuleCat : Type u_3))
      (ContinuousMap.comp
        (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
          C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
        (x.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))))
      (ContinuousMap.comp
        (↑(TopModuleCat.Hom.hom ((rep.ρ : (a : G) → End rep.V) g)) :
          C((↑rep.V.toModuleCat : Type u_3), (↑rep.V.toModuleCat : Type u_3)))
        (x_1.comp (↑(Homeomorph.mulLeft g⁻¹) : C(G, G))))

Tactic:
ext