awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
a :
  ∀
    (x :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u)),
    Eq (α :=
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
      ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))))) :
            (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
              (↑(unop
                    (op
                      (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                        { as := WalkingPair.left }))) :
                Type u))
          x :
        (↑(unop
              (op
                (Functor.obj
                  (Functor.obj (Functor.const (Discrete WalkingPair))
                    (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                  { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u))
      ((Hom.hom (S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)).unop :
            (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
              (↑(unop
                    (op
                      (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                        { as := WalkingPair.left }))) :
                Type u))
          x :
        (↑(unop
              (op
                (Functor.obj
                  (Functor.obj (Functor.const (Discrete WalkingPair))
                    (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                  { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u))
⊢ Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))) =
    S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u)
a :
  Eq (α :=
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u) ⊗[R]
      (↑(unop T) : Type u))
    (x ⊗ₜ[R] 1 :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u) ⊗[R]
        (↑(unop T) : Type u))
    (x ⊗ₜ[R] (algebraMap R (↑(unop T) : Type u) : (a : R) → (↑(unop T) : Type u)) 1 :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u) ⊗[R]
        (↑(unop T) : Type u))
⊢ Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.left : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inl ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (S ◁ IsTerminal.from (terminalOpOfInitial isInitialSelf) T ≫ Iso.hom (ρ_ S)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.left }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.left }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u))

Tactic:
change x ⊗ₜ 1 = x ⊗ₜ algebraMap R T.unop 1

Premises used: Algebra.algebraMap, CommAlgCat.carrier, OfNat.ofNat, DFunLike.coe, Opposite.unop
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) : Type u)
⊢ Eq (α :=
    (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
        Type u) ⊗[R]
      (↑(unop T) : Type u))
    (x ⊗ₜ[R] 1 :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u) ⊗[R]
        (↑(unop T) : Type u))
    (x ⊗ₜ[R] (algebraMap R (↑(unop T) : Type u) : (a : R) → (↑(unop T) : Type u)) 1 :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.left : Discrete WalkingPair }))) :
          Type u) ⊗[R]
        (↑(unop T) : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
a :
  ∀
    (x :
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u)),
    Eq (α :=
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
      ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))))) :
            (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
              (↑(unop
                    (op
                      (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                        { as := WalkingPair.right }))) :
                Type u))
          x :
        (↑(unop
              (op
                (Functor.obj
                  (Functor.obj (Functor.const (Discrete WalkingPair))
                    (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                  { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))
      ((Hom.hom (IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)).unop :
            (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
              (↑(unop
                    (op
                      (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                        { as := WalkingPair.right }))) :
                Type u))
          x :
        (↑(unop
              (op
                (Functor.obj
                  (Functor.obj (Functor.const (Discrete WalkingPair))
                    (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                  { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))
⊢ Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))) =
    IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u)
a :
  Eq (α :=
    (↑(unop S) : Type u) ⊗[R]
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u))
    (1 ⊗ₜ[R] x :
      (↑(unop S) : Type u) ⊗[R]
        (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))
    ((algebraMap R (↑(unop S) : Type u) : (a : R) → (↑(unop S) : Type u)) 1 ⊗ₜ[R] x :
      (↑(unop S) : Type u) ⊗[R]
        (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))
⊢ Eq (α :=
    (↑(unop
          (op
            (Functor.obj
              (Functor.obj (Functor.const (Discrete WalkingPair))
                (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
              { as := WalkingPair.right : Discrete WalkingPair }))) :
      Type u))
    ((Hom.hom (Quiver.Hom.unop (Quiver.Hom.op (BinaryCofan.inr ((unop S).binaryCofan (unop T))))) :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))
    ((Hom.hom (IsTerminal.from (terminalOpOfInitial isInitialSelf) S ▷ T ≫ Iso.hom (λ_ T)).unop :
          (a : (↑(unop (op ((pair (unop S) (unop T)).obj { as := WalkingPair.right }))) : Type u)) →
            (↑(unop
                  (op
                    (((Functor.const (Discrete WalkingPair)).obj ((unop S).binaryCofan (unop T)).pt).obj
                      { as := WalkingPair.right }))) :
              Type u))
        x :
      (↑(unop
            (op
              (Functor.obj
                (Functor.obj (Functor.const (Discrete WalkingPair))
                  (Cocone.pt (F := pair (unop S) (unop T)) ((unop S).binaryCofan (unop T))))
                { as := WalkingPair.right : Discrete WalkingPair }))) :
        Type u))

Tactic:
change 1 ⊗ₜ x = algebraMap R S.unop 1 ⊗ₜ x

Premises used: Algebra.algebraMap, CommAlgCat.carrier, OfNat.ofNat, DFunLike.coe, Opposite.unop
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C D : CommAlgCat R
S T : (CommAlgCat R)ᵒᵖ
x : (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u)
⊢ Eq (α :=
    (↑(unop S) : Type u) ⊗[R]
      (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) : Type u))
    (1 ⊗ₜ[R] x :
      (↑(unop S) : Type u) ⊗[R]
        (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))
    ((algebraMap R (↑(unop S) : Type u) : (a : R) → (↑(unop S) : Type u)) 1 ⊗ₜ[R] x :
      (↑(unop S) : Type u) ⊗[R]
        (↑(unop (op (Functor.obj (pair (unop S) (unop T)) { as := WalkingPair.right : Discrete WalkingPair }))) :
          Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : (CommAlgCat R)ᵒᵖ
⊢ Hom.hom (Quiver.Hom.unop (fst A B)) = includeLeft

Tactic:
rfl

Premises used: Algebra.TensorProduct.includeLeft, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B : (CommAlgCat R)ᵒᵖ
⊢ Hom.hom (Quiver.Hom.unop (snd A B)) = includeRight

Tactic:
rfl

Premises used: rfl, Algebra.TensorProduct.includeRight
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A : (CommAlgCat R)ᵒᵖ
⊢ Hom.hom (Quiver.Hom.unop (toUnit A)) = Algebra.ofId R (↑(unop A) : Type u)

Tactic:
rfl

Premises used: Algebra.ofId, rfl
-- Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
A B C : (CommAlgCat R)ᵒᵖ
f : C ⟶ A
g : C ⟶ B
⊢ Hom.hom (Quiver.Hom.unop (CartesianMonoidalCategory.lift f g)) =
    Algebra.TensorProduct.lift (Hom.hom f.unop) (Hom.hom g.unop) ⋯

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, AlgHom.ofLinearMap, Algebra.TensorProduct.lift, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : CommRing X
inst_2 : Bialgebra R X
⊢ (↑(of R X) : Type v) = X

Tactic:
rfl

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

Tactic:
rfl

Premises used: BialgHom.id, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B C : CommBialgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
⊢ Hom.hom (f ≫ g) = (Hom.hom g).comp (Hom.hom f)

Tactic:
rfl

Premises used: BialgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : CommBialgCat.{v, u} R
a : (↑A : Type v)
⊢ (@ConcreteCategory.hom _ instCategory (fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v))
          carrier
          (fun (X Y : CommBialgCat.{v, u} R) ↦
            (BialgHom.funLike : FunLike ((↑X : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B C : CommBialgCat.{v, u} R
f : A ⟶ B
g : B ⟶ C
a : (↑A : Type v)
⊢ Eq (α := (↑C : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v)) (CC :=
            carrier) g :
          (a : (↑B : Type v)) → (↑C : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B : CommBialgCat.{v, u} R
f g : A ⟶ B
hf : Hom.hom f = Hom.hom g
⊢ f = g

Tactic:
Hom.ext hf

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : CommRing X
inst_2 : Bialgebra R X
inst_3 : CommRing Y
inst_4 : Bialgebra R Y
f : X →ₐc[R] Y
x : X
⊢ Eq (α := (↑(of R Y) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B : CommBialgCat.{v, u} R
e : A ≅ B
x : (↑A : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v)) (CC :=
          carrier) e.inv :
        (a : (↑B : Type v)) → (↑A : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B : CommBialgCat.{v, u} R
e : A ≅ B
x : (↑B : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v)) (CC :=
          carrier) e.hom :
        (a : (↑A : Type v)) → (↑B : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A : CommBialgCat.{v, u} R
⊢ Functor.obj
      (forget (CommBialgCat.{v, u} R) (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v))
        (CC := carrier))
      A =
    (↑A : Type v)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B C : CommBialgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Bialgebra R X
inst_3 : CommRing Y
inst_4 : Bialgebra R Y
inst_5 : CommRing Z
inst_6 : Bialgebra R Z
i : A ≅ B
x : (↑A : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v)) (CC :=
          carrier) i.inv :
        (a : (↑B : Type v)) → (↑A : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.CommBialgCat
Goal:
R : Type u
inst : CommRing R
A B C : CommBialgCat.{v, u} R
X Y Z : Type v
inst_1 : CommRing X
inst_2 : Bialgebra R X
inst_3 : CommRing Y
inst_4 : Bialgebra R Y
inst_5 : CommRing Z
inst_6 : Bialgebra R Z
i : A ≅ B
x : (↑B : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[R] (↑x2 : Type v)) (CC :=
          carrier) i.hom :
        (a : (↑A : Type v)) → (↑B : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommBialgCat.{v, u} R) ↦ (↑x1 : Type v) →ₐc[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.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:
(isoMk e).isIso_hom

Premises used: CommBialgCat.isoMk, CategoryTheory.Iso.isIso_hom, BialgHomClass.toBialgHom