awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₐc[R] B
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →ₐ[R] B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₐc[R] B
⊢ Eq (α := A →ₗ[R] B)
    (↑(↑f : A →ₐ[R] B) :
      [inst_7 : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)
    (↑f : [inst_7 : FunLike (A →ₐc[R] B) A B] → [SemilinearMapClass (A →ₐc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (α := A →ₐc[R] B) (β := A → B) (DFunLike.coe (β := fun (x : A) ↦ B))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₐc[R] B
⊢ Eq (α := (a : A) → B) (⇑φ₁ : (a : A) → B) (⇑φ₂ : (a : A) → B) ↔ φ₁ = φ₂

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (α := A →ₐc[R] B) (β := A →ₗc[R] B) CoalgHomClass.toCoalgHom

Tactic:
fun φ₁ φ₂ H => coe_fn_injective <|
    show ((φ₁ : A →ₗc[R] B) : A → B) = ((φ₂ : A →ₗc[R] B) : A → B) from congr_arg _ H

Premises used: BialgHom.coe_fn_injective, congr_arg, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (α := A →ₐc[R] B) toAlgHom

Tactic:
fun φ₁ φ₂ H => coe_fn_injective <|
    show ((φ₁ : A →ₐ[R] B) : A → B) = ((φ₂ : A →ₐ[R] B) : A → B) from congr_arg _ H

Premises used: BialgHom.coe_fn_injective, congr_arg, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
⊢ Injective (β := A →ₗ[R] B) fun (x : A →ₐc[R] B) ↦
    (↑x : [inst_7 : FunLike (A →ₐc[R] B) A B] → [SemilinearMapClass (A →ₐc[R] B) (RingHom.id R) A B] → A →ₗ[R] B)

Tactic:
CoalgHom.coe_linearMap_injective.comp coe_coalgHom_injective

Premises used: BialgHom.coe_coalgHom_injective, CoalgHom.coe_linearMap_injective, SemilinearMapClass.semilinearMap, Function.Injective.comp
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₐc[R] B
H : φ₁ = φ₂
x : A
⊢ Eq.{u_3 + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)

Tactic:
DFunLike.congr_fun H x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₐc[R] B
x y : A
h : x = y
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) y : B)

Tactic:
DFunLike.congr_arg φ h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ₁ φ₂ : A →ₐc[R] B
H : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((φ₁ : (a : A) → B) x : B) ((φ₂ : (a : A) → B) x : B)
⊢ φ₁ = φ₂

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
f g : R →ₐc[R] A
h : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 1 : A) ((g : (a : R) → A) 1 : A)
h₁ :
  Eq.{u_2 + 1} (α := A)
    (((fun (x : R →ₐc[R] A) ↦
              ((↑x :
                  [inst_4 : FunLike (R →ₐc[R] A) R A] →
                    [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
                R →ₗ[R] A))
            f :
          (a : R) → A)
        1 :
      A)
    (((fun (x : R →ₐc[R] A) ↦
              ((↑x :
                  [inst_4 : FunLike (R →ₐc[R] A) R A] →
                    [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
                R →ₗ[R] A))
            g :
          (a : R) → A)
        1 :
      A)
⊢ Eq (α := R →ₗ[R] A)
    ((fun (x : R →ₐc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₐc[R] A) R A] → [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      f)
    ((fun (x : R →ₐc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₐc[R] A) R A] → [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      g)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
f g : R →ₐc[R] A
h : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 1 : A) ((g : (a : R) → A) 1 : A)
⊢ Eq.{u_2 + 1} (α := A)
    (((fun (x : R →ₐc[R] A) ↦
              ((↑x :
                  [inst_4 : FunLike (R →ₐc[R] A) R A] →
                    [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
                R →ₗ[R] A))
            f :
          (a : R) → A)
        1 :
      A)
    (((fun (x : R →ₐc[R] A) ↦
              ((↑x :
                  [inst_4 : FunLike (R →ₐc[R] A) R A] →
                    [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
                R →ₗ[R] A))
            g :
          (a : R) → A)
        1 :
      A)

Tactic:
assumption
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₐc[R] B
h₀ :
  ∀ (x y : A),
    (f : (a : A) → B) (x + y) = HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
h₁ :
  ∀ (m : R) (x : A),
    { toFun := (⇑f : (a : A) → B), map_add' := h₀ : A →ₙ+ B }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := (⇑f : (a : A) → B), map_add' := h₀ : A →ₙ+ B }.toFun x)
h₂ : counit ∘ₗ { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁ : A →ₗ[R] B } = counit
h₃ :
  map { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁ : A →ₗ[R] B }
        { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁ : A →ₗ[R] B } ∘ₗ
      comul =
    comul ∘ₗ { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁ : A →ₗ[R] B }
h₄ :
  { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ :
          A →ₗc[R] B }.toFun
      1 =
    1
h₅ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ :
            A →ₗc[R] B }.toFun
        (x * y) =
      { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ :
              A →ₗc[R] B }.toFun
          x *
        { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ :
              A →ₗc[R] B }.toFun
          y
⊢ { toFun := (⇑f : (a : A) → B), map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃,
      map_one' := h₄, map_mul' := h₅ : A →ₐc[R] B } =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (CoalgHom.copy (↑f : A →ₗc[R] B) f' h).toFun 1 = 1

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
x y : A
⊢ (CoalgHom.copy (↑f : A →ₗc[R] B) f' h).toFun (x * y) =
    (CoalgHom.copy (↑f : A →ₗc[R] B) f' h).toFun x * (CoalgHom.copy (↑f : A →ₗc[R] B) f' h).toFun y

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
f : A →ₗc[R] B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := (a : A) → A) (⇑(BialgHom.id R A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := A →ₗc[R] A) (↑(BialgHom.id R A) : A →ₗc[R] A) (CoalgHom.id R A)

Tactic:
rfl

Premises used: CoalgHomClass.toCoalgHom, CoalgHom.id, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := A →ₐ[R] A) (↑(BialgHom.id R A) : A →ₐ[R] A) (AlgHom.id R A)

Tactic:
rfl

Premises used: AlgHom.id, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
φ₁ : B →ₐc[R] C
φ₂ : A →ₐc[R] B
⊢ Eq (α := (a : A) → C) (⇑(φ₁.comp φ₂) : (a : A) → C)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := B) (⇑φ₁ : (a : B) → C) (⇑φ₂ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
φ₁ : B →ₐc[R] C
φ₂ : A →ₐc[R] B
⊢ Eq (α := A →ₗc[R] C) (↑(φ₁.comp φ₂) : A →ₗc[R] C) (CoalgHom.comp (↑φ₁ : B →ₗc[R] C) (↑φ₂ : A →ₗc[R] B))

Tactic:
rfl

Premises used: CoalgHom.comp, CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
inst_7 : CoalgebraStruct R A
inst_8 : CoalgebraStruct R B
inst_9 : CoalgebraStruct R C
φ₁ : B →ₐc[R] C
φ₂ : A →ₐc[R] B
⊢ (↑(φ₁.comp φ₂) : A →ₐ[R] C) = (↑φ₁ : B →ₐ[R] C).comp (↑φ₂ : A →ₐ[R] B)

Tactic:
rfl

Premises used: BialgHom.toAlgHom, AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₐc[R] B
⊢ φ.comp (BialgHom.id R A) = φ

Tactic:
ext fun _x => rfl

Premises used: BialgHom.ext, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₐc[R] B
⊢ comp (BialgHom.id R B) φ = φ

Tactic:
ext fun _x => rfl

Premises used: BialgHom.ext, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
φ₁ : C →ₐc[R] D
φ₂ : B →ₐc[R] C
φ₃ : A →ₐc[R] B
⊢ (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)

Tactic:
ext fun _x => rfl

Premises used: BialgHom.ext, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CoalgebraStruct R A
inst_6 : CoalgebraStruct R B
φ : A →ₐc[R] B
R' : Type u_6
inst_7 : SMul R' A
inst_8 : SMul R' B
inst_9 : LinearMap.CompatibleSMul A B R' R
r : R'
x : A
⊢ (φ : (a : A) → B) (r • x) = HSMul.hSMul (β := B) r ((φ : (a : A) → B) x : B)

Tactic:
φ.toLinearMap.map_smul_of_tower r x

Premises used: CoalgHom.toLinearMap, BialgHom.toCoalgHom, LinearMap.map_smul_of_tower
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
x : A
⊢ (1 : (a : A) → A) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
φ ψ : A →ₐc[R] A
x : A
⊢ Eq (α := A) ((φ * ψ : (a : A) → A) x : A) ((φ : (a : A) → A) ((ψ : (a : A) → A) x : A) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
⊢ AlgHom.comp (counitAlgHom R B) (↑f : A →ₐ[R] B) = counitAlgHom R A

Tactic:
AlgHom.toLinearMap_injective (CoalgHomClass.counit_comp f)

Premises used: AlgHom.toLinearMap_injective, CoalgHomClass.counit_comp
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
⊢ AlgHom.comp
      (Algebra.TensorProduct.map (↑f : A →ₐ[R] B) (↑f : A →ₐ[R] B) : AlgHom.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B))
      (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (comulAlgHom R B) (↑f : A →ₐ[R] B)

Tactic:
AlgHom.toLinearMap_injective (CoalgHomClass.map_comp_comul f)

Premises used: AlgHom.toLinearMap_injective, CoalgHomClass.map_comp_comul
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := R →ₐ[R] R) (AlgHom.comp (counitAlgHom R A) (Algebra.ofId R A)) (counitAlgHom R R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := AlgHom.{u_1, u_1, u_2} R R (A ⊗[R] A))
    (AlgHom.comp
        (Algebra.TensorProduct.map (Algebra.ofId R A) (Algebra.ofId R A) :
          AlgHom.{u_1, u_1, u_2} R (R ⊗[R] R) (A ⊗[R] A))
        (comulAlgHom R R : R →ₐ[R] R ⊗[R] R) :
      AlgHom.{u_1, u_1, u_2} R R (A ⊗[R] A))
    (AlgHom.comp (comulAlgHom R A) (Algebra.ofId R A) : AlgHom.{u_1, u_1, u_2} R R (A ⊗[R] A))

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
x : A
⊢ Eq.{u_1 + 1} (α := R) ((counitBialgHom R A : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Eq (α := A →ₗc[R] R) (↑(counitBialgHom R A) : A →ₗc[R] R) (counitCoalgHom R A)

Tactic:
rfl

Premises used: Coalgebra.counitCoalgHom, CoalgHomClass.toCoalgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →ₐc[R] R) (counitBialgHom R R) (BialgHom.id R R)

Tactic:
rfl

Premises used: BialgHom.id, Coalgebra.counitCoalgHom, CoalgHom.id, Bialgebra.counitBialgHom, rfl
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
⊢ Subsingleton (A →ₐc[R] R)

Tactic:
⟨fun _ _ => BialgHom.coe_coalgHom_injective (Subsingleton.elim _ _)⟩

Premises used: BialgHom.coe_coalgHom_injective, CoalgHomClass.toCoalgHom, Subsingleton.intro, Subsingleton.elim
-- Module: Mathlib.RingTheory.Bialgebra.Hom
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
f g : A →ₐc[R] R
⊢ f = g

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
⊢ Eq.{u_1 + 1} (α := R) ((CoalgebraStruct.counit : (a : A[M]) → R) 1 : R) (1 : R)

Tactic:
simp only [one_def, counit_single, Bialgebra.counit_one]

Premises used: MonoidAlgebra.one_def, Bialgebra.counit_one, MonoidAlgebra.counit_single
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
H :
  ∀ (x : M) (x_1 : A) (x_2 : M) (x_3 : A),
    Eq.{u_1 + 1} (α := R)
      (((LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.counit ∘ₗ lsingle x : (a : A) → A[M] →ₗ[R] R) x_1 ∘ₗ
              lsingle x_2 :
            (a : A) → R)
          x_3 :
        R)
      (((LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit ∘ₗ lsingle x :
                  (a : A) → A[M] →ₗ[R] R)
                x_1 ∘ₗ
              lsingle x_2 :
            (a : A) → R)
          x_3 :
        R)
⊢ Eq (α := A[M] →ₗ[R] A[M] →ₗ[R] R) (LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.counit)
    (LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
x : M
x_1 : A
x_2 : M
x_3 : A
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.counit ∘ₗ lsingle x : (a : A) → A[M] →ₗ[R] R) x_1 ∘ₗ
            lsingle x_2 :
          (a : A) → R)
        x_3 :
      R)
    (((LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit ∘ₗ lsingle x :
                (a : A) → A[M] →ₗ[R] R)
              x_1 ∘ₗ
            lsingle x_2 :
          (a : A) → R)
        x_3 :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
⊢ Eq (α := TensorProduct R A[M] A[M]) ((CoalgebraStruct.comul : (a : A[M]) → TensorProduct R A[M] A[M]) 1) 1

Tactic:
simp only [one_def, comul_single, Bialgebra.comul_one, Algebra.TensorProduct.one_def,
      TensorProduct.map_tmul, lsingle_apply]

Premises used: MonoidAlgebra.lsingle_apply, MonoidAlgebra.comul_single, TensorProduct.map_tmul, MonoidAlgebra.one_def, Bialgebra.comul_one, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
H :
  ∀ (a : M) (b : A) (c : M) (d : A),
    Eq (α := TensorProduct R A[M] A[M])
      (((LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.comul ∘ₗ lsingle a :
                  (a : A) → A[M] →ₗ[R] TensorProduct R A[M] A[M])
                b ∘ₗ
              lsingle c :
            (a : A) → TensorProduct R A[M] A[M])
          d :
        TensorProduct R A[M] A[M])
      (((LinearMap.compl₁₂ (LinearMap.mul R (TensorProduct R A[M] A[M])) CoalgebraStruct.comul CoalgebraStruct.comul ∘ₗ
                    lsingle a :
                  (a : A) → A[M] →ₗ[R] TensorProduct R A[M] A[M])
                b ∘ₗ
              lsingle c :
            (a : A) → TensorProduct R A[M] A[M])
          d :
        TensorProduct R A[M] A[M])
⊢ Eq (α := A[M] →ₗ[R] A[M] →ₗ[R] TensorProduct R A[M] A[M])
    (LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.comul)
    (LinearMap.compl₁₂ (LinearMap.mul R (TensorProduct R A[M] A[M])) CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
ext a b c d