awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : BialgCat.{v, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.toBialgHom (f ≫ g) = (Hom.toBialgHom g).comp (Hom.toBialgHom f)

Tactic:
rfl

Premises used: BialgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
M : BialgCat.{v, u} R
⊢ Hom.toBialgHom (𝟙 M) = BialgHom.id R M.carrier

Tactic:
rfl

Premises used: BialgHom.id, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : BialgCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (BialgCat.{u_1, u} R) (FC := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier) (AlgCat.{u_1, u} R) (FD := fun (x1 x2 : AlgCat.{u_1, u} R) ↦ (↑x1 : Type u_1) →ₐ[R] (↑x2 : Type u_1))
        (CD := AlgCat.carrier))
      X =
    AlgCat.of R X.carrier

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : BialgCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (BialgCat.{u_1, u} R) (FC := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier) (CoalgCat.{u_1, u} R) (FD := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CD := fun (X : CoalgCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)))
      X =
    CoalgCat.of R X.carrier

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{u_1, u} R
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (forget₂ (BialgCat.{u_1, u} R) (FC := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
          carrier) (CoalgCat.{u_1, u} R) (FD := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
          (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CD := fun (X : CoalgCat.{u_1, u} R) ↦
          (↑X.toModuleCat : Type u_1)))
        X ⟶
      Functor.obj
        (forget₂ (BialgCat.{u_1, u} R) (FC := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
          carrier) (CoalgCat.{u_1, u} R) (FD := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
          (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CD := fun (X : CoalgCat.{u_1, u} R) ↦
          (↑X.toModuleCat : Type u_1)))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ (BialgCat.{u_1, u} R) (FC := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier) (CoalgCat.{u_1, u} R) (FD := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CD := fun (X : CoalgCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)))
      f)
    (CoalgCat.ofHom (↑(Hom.toBialgHom f) : X.carrier →ₗc[R] Y.carrier))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : Bialgebra R X
⊢ Eq (α := Iso (C := BialgCat.{v, u} R) (of R X) (of R X)) (toBialgIso (refl R X)) (Iso.refl (of R X))

Tactic:
rfl

Premises used: BialgHom.id, CategoryTheory.Iso.refl, BialgEquiv.toBialgIso, BialgHomClass.toBialgHom, CoalgHom.id, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : Ring X
inst_2 : Ring Y
inst_3 : Bialgebra R X
inst_4 : Bialgebra R Y
e : X ≃ₐc[R] Y
⊢ e.symm.toBialgIso = e.toBialgIso.symm

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, BialgEquiv.toBialgIso, CoalgEquiv.symm, BialgEquiv.symm, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : Ring X
inst_2 : Ring Y
inst_3 : Ring Z
inst_4 : Bialgebra R X
inst_5 : Bialgebra R Y
inst_6 : Bialgebra R Z
e : X ≃ₐc[R] Y
f : Y ≃ₐc[R] Z
⊢ (e.trans f).toBialgIso = e.toBialgIso ≪≫ f.toBialgIso

Tactic:
rfl

Premises used: CoalgHom.comp, BialgEquiv.toBialgIso, CategoryTheory.Iso.trans, BialgHom.comp, BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{v, u} R
i : X ≅ Y
⊢ (↑i.toBialgEquiv : X.carrier →ₐc[R] Y.carrier) = i.hom.toBialgHom'

Tactic:
rfl

Premises used: BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : BialgCat.{v, u} R
⊢ toBialgEquiv (refl X) = BialgEquiv.refl R X.carrier

Tactic:
rfl

Premises used: CoalgEquiv.refl, CategoryTheory.Iso.toBialgEquiv, CoalgHom.id, rfl, BialgEquiv.refl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{v, u} R
e : X ≅ Y
⊢ e.symm.toBialgEquiv = e.toBialgEquiv.symm

Tactic:
rfl

Premises used: CoalgEquiv.symm, BialgEquiv.symm, CategoryTheory.Iso.toBialgEquiv, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : BialgCat.{v, u} R
e : X ≅ Y
f : Y ≅ Z
⊢ (e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv

Tactic:
rfl

Premises used: BialgEquiv.trans, CoalgEquivClass.toCoalgEquiv, CoalgHom.comp, CoalgHomClass.toCoalgHom, CategoryTheory.Iso.toBialgEquiv, CoalgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier))
    X ≅
  Functor.obj
    (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
⟨e.toBialgIso.isIso_hom.1⟩

Premises used: CategoryTheory.IsIso.mk, CategoryTheory.IsIso.out
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier))
    X ≅
  Functor.obj
    (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC := carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (BialgCat.{v, u} R) (FC := fun (x1 x2 : BialgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact ⟨e.toBialgIso.isIso_hom.1⟩
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α : Type u_1
inst : BooleanRing α
⊢ (↑{ carrier := α, booleanRing := inst : BoolRing.{u_1} } : Type u_1) = α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
R S : BoolRing
f g : R ⟶ S
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

Premises used: BoolRing.Hom.ext
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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))
⊢ { hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) : α.Hom β } ≫
      { hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) } =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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:
e.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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:
exact e.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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))
⊢ { hom' := (↑e.symm : (↑β : Type u) →+* (↑α : Type u)) : β.Hom α } ≫
      { hom' := (↑e : (↑α : Type u) →+* (↑β : Type u)) } =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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:
e.apply_symm_apply _

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.BoolRing
Goal:
α β : BoolRing
e : (↑α : Type u) ≃+* (↑β : Type u)
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:
exact e.apply_symm_apply _

Premises used: RingEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : CoalgCat.{v, u} R
⊢ ModuleCat.of R (↑X.toModuleCat : Type v) = X.toModuleCat

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : Coalgebra R X
⊢ Eq.{v + 1} (α :=
    (↑(toModuleCat (of R X)) : Type v) →ₗ[R]
      TensorProduct R (↑(toModuleCat (of R X)) : Type v) (↑(toModuleCat (of R X)) : Type v))
    comul comul

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : Coalgebra R X
⊢ Eq (α := LinearMap.{u, u, v, u} (RingHom.id R) (↑(toModuleCat (of R X)) : Type v) R) counit counit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
V W : CoalgCat.{v, u} R
x x_1 : V.Hom W
f g : (↑V.toModuleCat : Type v) →ₗc[R] (↑W.toModuleCat : Type v)
h : { toCoalgHom' := f : V.Hom W }.toCoalgHom' = { toCoalgHom' := g }.toCoalgHom'
⊢ { toCoalgHom' := f : V.Hom W } = { toCoalgHom' := g }

Tactic:
congr
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
M N : CoalgCat.{v, u} R
f g : M ⟶ N
h : Hom.toCoalgHom f = Hom.toCoalgHom g
⊢ f = g

Tactic:
Hom.ext h

Premises used: CoalgCat.Hom.ext
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
M N U : CoalgCat.{v, u} R
f : M ⟶ N
g : N ⟶ U
⊢ Hom.toCoalgHom (f ≫ g) = (Hom.toCoalgHom g).comp (Hom.toCoalgHom f)

Tactic:
rfl

Premises used: CoalgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
M : CoalgCat.{v, u} R
⊢ Hom.toCoalgHom (𝟙 M) = CoalgHom.id R (↑M.toModuleCat : Type v)

Tactic:
rfl

Premises used: CoalgHom.id, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : CoalgCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (CoalgCat.{u_1, u} R) (FC := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : CoalgCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
      X =
    ModuleCat.of R (↑X.toModuleCat : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat.{u_1, u} R
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (forget₂ (CoalgCat.{u_1, u} R) (FC := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
          (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : CoalgCat.{u_1, u} R) ↦
          (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
        X ⟶
      Functor.obj
        (forget₂ (CoalgCat.{u_1, u} R) (FC := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
          (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : CoalgCat.{u_1, u} R) ↦
          (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
        Y)
    (CategoryTheory.Functor.map
      (forget₂ (CoalgCat.{u_1, u} R) (FC := fun (x1 x2 : CoalgCat.{u_1, u} R) ↦
        (↑x1.toModuleCat : Type u_1) →ₗc[R] (↑x2.toModuleCat : Type u_1)) (CC := fun (X : CoalgCat.{u_1, u} R) ↦
        (↑X.toModuleCat : Type u_1)) (ModuleCat.{u_1, u} R) (FD := fun (x1 x2 : ModuleCat.{u_1, u} R) ↦
        (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CD := ModuleCat.carrier))
      f)
    (ModuleCat.ofHom
      (↑(Hom.toCoalgHom f) :
        [inst_1 :
            FunLike ((↑X.toModuleCat : Type u_1) →ₗc[R] (↑Y.toModuleCat : Type u_1)) (↑X.toModuleCat : Type u_1)
              (↑Y.toModuleCat : Type u_1)] →
          [SemilinearMapClass ((↑X.toModuleCat : Type u_1) →ₗc[R] (↑Y.toModuleCat : Type u_1)) (RingHom.id R)
                (↑X.toModuleCat : Type u_1) (↑Y.toModuleCat : Type u_1)] →
            (↑X.toModuleCat : Type u_1) →ₗ[R] (↑Y.toModuleCat : Type u_1)))

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : Coalgebra R X
⊢ Eq (α := Iso (C := CoalgCat.{v, u} R) (of R X) (of R X)) (toCoalgIso (refl R X)) (Iso.refl (of R X))

Tactic:
rfl

Premises used: CoalgEquiv.toCoalgIso, CategoryTheory.Iso.refl, CoalgHomClass.toCoalgHom, CoalgHom.id, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : AddCommGroup Y
inst_4 : Module R Y
inst_5 : Coalgebra R X
inst_6 : Coalgebra R Y
e : X ≃ₗc[R] Y
⊢ e.symm.toCoalgIso = e.toCoalgIso.symm

Tactic:
rfl

Premises used: CoalgEquiv.toCoalgIso, CoalgEquiv.symm, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : AddCommGroup X
inst_2 : Module R X
inst_3 : AddCommGroup Y
inst_4 : Module R Y
inst_5 : AddCommGroup Z
inst_6 : Module R Z
inst_7 : Coalgebra R X
inst_8 : Coalgebra R Y
inst_9 : Coalgebra R Z
e : X ≃ₗc[R] Y
f : Y ≃ₗc[R] Z
⊢ (e.trans f).toCoalgIso = e.toCoalgIso ≪≫ f.toCoalgIso

Tactic:
rfl

Premises used: CoalgEquiv.toCoalgIso, CoalgHom.comp, CoalgHomClass.toCoalgHom, CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat.{v, u} R
i : X ≅ Y
⊢ (↑i.toCoalgEquiv : (↑X.toModuleCat : Type v) →ₗc[R] (↑Y.toModuleCat : Type v)) = CoalgCat.Hom.toCoalgHom i.hom

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : CoalgCat.{v, u} R
⊢ toCoalgEquiv (refl X) = CoalgEquiv.refl R (↑X.toModuleCat : Type v)

Tactic:
rfl

Premises used: CategoryTheory.Iso.toCoalgEquiv, CoalgEquiv.refl, CoalgHom.id, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat.{v, u} R
e : X ≅ Y
⊢ e.symm.toCoalgEquiv = e.toCoalgEquiv.symm

Tactic:
rfl

Premises used: CategoryTheory.Iso.toCoalgEquiv, CoalgEquiv.symm, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : CoalgCat.{v, u} R
e : X ≅ Y
f : Y ≅ Z
⊢ (e ≪≫ f).toCoalgEquiv = e.toCoalgEquiv.trans f.toCoalgEquiv

Tactic:
rfl

Premises used: CoalgHom.comp, CategoryTheory.Iso.toCoalgEquiv, CoalgHomClass.toCoalgHom, CoalgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      X)
    (CategoryTheory.Functor.map
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      f)
i : Functor.obj
    (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
      (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
      (↑X.toModuleCat : Type v)))
    X ≅
  Functor.obj
    (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
      (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
      (↑X.toModuleCat : Type v)))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      f)
e : (↑X.toModuleCat : Type v) ≃ₗc[R] (↑Y.toModuleCat : Type v) :=
  let __src := Hom.toCoalgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
⟨e.toCoalgIso.isIso_hom.1⟩

Premises used: CategoryTheory.IsIso.mk, CategoryTheory.IsIso.out
-- Module: Mathlib.Algebra.Category.CoalgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : CoalgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      X)
    (CategoryTheory.Functor.map
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      f)
i : Functor.obj
    (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
      (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
      (↑X.toModuleCat : Type v)))
    X ≅
  Functor.obj
    (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
      (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
      (↑X.toModuleCat : Type v)))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (CoalgCat.{v, u} R) (FC := fun (x1 x2 : CoalgCat.{v, u} R) ↦
        (↑x1.toModuleCat : Type v) →ₗc[R] (↑x2.toModuleCat : Type v)) (CC := fun (X : CoalgCat.{v, u} R) ↦
        (↑X.toModuleCat : Type v)))
      f)
e : (↑X.toModuleCat : Type v) ≃ₗc[R] (↑Y.toModuleCat : Type v) :=
  let __src := Hom.toCoalgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯ }
⊢ IsIso f

Tactic:
exact ⟨e.toCoalgIso.isIso_hom.1⟩
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
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 R)) (𝒞 := ModuleCat.moduleCategory R))
            (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.ofHom CoalgebraStruct.counit ▷ ModuleCat.of R (↑X.toModuleCat : Type u))))
    (ModuleCat.Hom.hom (Iso.inv (λ_ (ModuleCat.of R (↑X.toModuleCat : Type u)))))

Tactic:
simpa using Coalgebra.rTensor_counit_comp_comul

Premises used: Coalgebra.rTensor_counit_comp_comul
-- Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
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))
            ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R))) :
        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.counit)))
    (ModuleCat.Hom.hom (Iso.inv (ρ_ (ModuleCat.of R (↑X.toModuleCat : Type u)))))

Tactic:
simpa using Coalgebra.lTensor_counit_comp_comul

Premises used: Coalgebra.lTensor_counit_comp_comul