awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
h :
  Eq (α := A ⊗[R] A →ₗ[R] A) (antipode R ∘ₗ LinearMap.mul' R A)
    (LinearMap.mul' R A ∘ₗ
      TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))
⊢ (antipode R : (a : A) → A) (a * b) =
    HMul.hMul (α := A) (β := A) ((antipode R : (a : A) → A) b : A) ((antipode R : (a : A) → A) a : A)

Tactic:
congr(($h) (a ⊗ₜ b))

Premises used: congrArg, id, TensorProduct.tmul, DFunLike.coe
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
h :
  Eq (α := A ⊗[R] A →ₗ[R] A) (antipode R ∘ₗ LinearMap.mul' R A)
    (LinearMap.mul' R A ∘ₗ
      TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))
⊢ (antipode R : (a : A) → A) (a * b) =
    HMul.hMul (α := A) (β := A) ((antipode R : (a : A) → A) b : A) ((antipode R : (a : A) → A) a : A)

Tactic:
exact congr(($h) (a ⊗ₜ b))
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
suffices :
  Eq (α := A ⊗[R] A →ₗ[R] A) (antipode R ∘ₗ LinearMap.mul' R A)
    (LinearMap.mul' R A ∘ₗ
      TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))
⊢ (antipode R : (a : A) → A) (a * b) =
    HMul.hMul (α := A) (β := A) ((antipode R : (a : A) → A) b : A) ((antipode R : (a : A) → A) a : A)

Tactic:
suffices h : antipode R ∘ₗ LinearMap.mul' R A =
      LinearMap.mul' R A ∘ₗ TensorProduct.map (antipode R) (antipode R) ∘ₗ
        TensorProduct.comm R A A by
    exact congr(($h) (a ⊗ₜ b))
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
⊢ Eq (α := A ⊗[R] A →ₗ[R] A) (antipode R ∘ₗ LinearMap.mul' R A)
    (LinearMap.mul' R A ∘ₗ
      TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))

Tactic:
toConv_injective
    (left_inv_eq_right_inv
      (b := toConv (antipode R ∘ₗ LinearMap.mul' R A))
      (a := toConv (LinearMap.mul' R A))
      (c := toConv (LinearMap.mul' R A ∘ₗ TensorProduct.map (antipode R) (antipode R) ∘ₗ
        TensorProduct.comm R A A))
      ?_ ?_)

Premises used: left_inv_eq_right_inv, WithConv.toConv_injective
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
refine_1 :
  HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A))
      (toConv (LinearMap.mul' R A)) =
    1
refine_2 :
  HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (LinearMap.mul' R A))
      (toConv
        (LinearMap.mul' R A ∘ₗ
          TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))) =
    1
⊢ Eq (α := A ⊗[R] A →ₗ[R] A) (antipode R ∘ₗ LinearMap.mul' R A)
    (LinearMap.mul' R A ∘ₗ
      TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))

Tactic:
refine toConv_injective
    (left_inv_eq_right_inv
      (b := toConv (antipode R ∘ₗ LinearMap.mul' R A))
      (a := toConv (LinearMap.mul' R A))
      (c := toConv (LinearMap.mul' R A ∘ₗ TensorProduct.map (antipode R) (antipode R) ∘ₗ
        TensorProduct.comm R A A))
      ?_ ?_)

Premises used: left_inv_eq_right_inv, WithConv.toConv_injective
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
⊢ HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A))
      (toConv (LinearMap.mul' R A)) =
    1

Tactic:
WithConv.ext (TensorProduct.ext' fun x y => ?_)

Premises used: WithConv.ext, TensorProduct.ext'
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
refine_1 :
  ∀ (x y : A),
    Eq (α := A)
      (((HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A))
                (toConv (LinearMap.mul' R A))).ofConv :
            (a : A ⊗[R] A) → A)
          (x ⊗ₜ[R] y) :
        A)
      ((ofConv 1 : (a : A ⊗[R] A) → A) (x ⊗ₜ[R] y) : A)
⊢ HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A))
      (toConv (LinearMap.mul' R A)) =
    1

Tactic:
refine WithConv.ext (TensorProduct.ext' fun x y => ?_)

Premises used: WithConv.ext, TensorProduct.ext'
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
refine_1 :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            ((comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] (A ⊗[R] A)) (x ⊗ₜ[R] y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    (((HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A))
              (toConv (LinearMap.mul' R A))).ofConv :
          (a : A ⊗[R] A) → A)
        (x ⊗ₜ[R] y) :
      A)
    ((ofConv 1 : (a : A ⊗[R] A) → A) (x ⊗ₜ[R] y) : A)

Tactic:
simp only [LinearMap.convMul_apply, LinearMap.convOne_apply]

Premises used: LinearMap.convOne_apply, LinearMap.convMul_apply
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
refine_1 :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                  A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
                (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
              ((comul : (a : A) → A ⊗[R] A) x ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            ((comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] (A ⊗[R] A)) (x ⊗ₜ[R] y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
rw [TensorProduct.comul_tmul]

Premises used: TensorProduct.comul_tmul
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
rw :
  ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
      ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
            (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
          (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
            ((∑ i ∈ ℛx.index, ℛx.left i ⊗ₜ[R] ℛx.right i) ⊗ₜ[R] ∑ i ∈ ℛy.index, ℛy.left i ⊗ₜ[R] ℛy.right i)) :
        A ⊗[R] A) :
    A)
| ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
      ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
            (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
          (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
            ((comul : (a : A) → A ⊗[R] A) x ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) y)) :
        A ⊗[R] A) :
    A)

Tactic:
rw [← ℛx.eq, ← ℛy.eq]

Premises used: Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
refine_1 :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                  A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
                (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
              ((∑ i ∈ ℛx.index, ℛx.left i ⊗ₜ[R] ℛx.right i) ⊗ₜ[R] ∑ i ∈ ℛy.index, ℛy.left i ⊗ₜ[R] ℛy.right i)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                  A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
                (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
              ((comul : (a : A) → A ⊗[R] A) x ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
conv_lhs => rw [← ℛx.eq, ← ℛy.eq]

Premises used: Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
refine_1 :
  Eq (α := A)
    (∑ x_1 ∈ ℛy.index,
        ∑ x_2 ∈ ℛx.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left x_2 * ℛy.left x_1) : A)
            (ℛx.right x_2 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (antipode R ∘ₗ LinearMap.mul' R A) (LinearMap.mul' R A) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                  A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
                (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
              ((∑ i ∈ ℛx.index, ℛx.left i ⊗ₜ[R] ℛx.right i) ⊗ₜ[R] ∑ i ∈ ℛy.index, ℛy.left i ⊗ₜ[R] ℛy.right i)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
simp only [TensorProduct.sum_tmul, TensorProduct.tmul_sum, map_sum,
      TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, TensorProduct.map_tmul,
      LinearMap.mul'_apply, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, LinearMap.mul'_apply, map_sum, TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.map_tmul, TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
refine_1 :
  Eq (α := A)
    (∑ y_1 ∈ ℛx.index,
        ∑ x_1 ∈ ℛy.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A)
            (ℛx.right y_1 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    (∑ x_1 ∈ ℛy.index,
        ∑ x_2 ∈ ℛx.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left x_2 * ℛy.left x_1) : A)
            (ℛx.right x_2 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
refine_1 :
  ∑ y_1 ∈ ℛx.index,
      ∑ x_1 ∈ ℛy.index,
        HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A) (ℛx.right y_1 * ℛy.right x_1) =
    HSMul.hSMul (β := A) (HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) y : R) ((counit : (a : A) → R) x : R)) 1
⊢ Eq (α := A)
    (∑ y_1 ∈ ℛx.index,
        ∑ x_1 ∈ ℛy.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A)
            (ℛx.right y_1 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
simp only [TensorProduct.counit_tmul, Algebra.algebraMap_eq_smul_one]

Premises used: TensorProduct.counit_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((LinearMap.rTensor A (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) (x * y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) (x * y) : R) : A)

Tactic:
have key := mul_antipode_rTensor_comul_apply (R := R) (x * y)
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
key :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((LinearMap.rTensor A (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A) ((comul : (a : A) → A ⊗[R] A) (x * y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) (x * y) : R) : A)
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((LinearMap.rTensor A (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
            (HMul.hMul (α := A ⊗[R] A) (∑ i ∈ ℛx.index, ℛx.left i ⊗ₜ[R] ℛx.right i)
              (∑ i ∈ ℛy.index, ℛy.left i ⊗ₜ[R] ℛy.right i)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) (x * y) : R) : A)

Tactic:
rw [Bialgebra.comul_mul, ← ℛx.eq, ← ℛy.eq] at key

Premises used: Bialgebra.comul_mul, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
key :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((LinearMap.rTensor A (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
            (HMul.hMul (α := A ⊗[R] A) (∑ i ∈ ℛx.index, ℛx.left i ⊗ₜ[R] ℛx.right i)
              (∑ i ∈ ℛy.index, ℛy.left i ⊗ₜ[R] ℛy.right i)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) (x * y) : R) : A)
⊢ Eq (α := A)
    (∑ x_1 ∈ ℛy.index,
        ∑ x_2 ∈ ℛx.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left x_2 * ℛy.left x_1) : A)
            (ℛx.right x_2 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A)
        (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) :
      A)

Tactic:
simp only [Finset.sum_mul, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul,
      map_sum, LinearMap.rTensor_tmul, LinearMap.mul'_apply, Bialgebra.counit_mul] at key

Premises used: Finset.mul_sum, LinearMap.rTensor_tmul, LinearMap.mul'_apply, Algebra.TensorProduct.tmul_mul_tmul, map_sum, Bialgebra.counit_mul, Finset.sum_mul
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
key :
  Eq (α := A)
    (∑ x_1 ∈ ℛy.index,
        ∑ x_2 ∈ ℛx.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left x_2 * ℛy.left x_1) : A)
            (ℛx.right x_2 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A)
        (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) :
      A)
⊢ Eq (α := A)
    (∑ y_1 ∈ ℛx.index,
        ∑ x_1 ∈ ℛy.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A)
            (ℛx.right y_1 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A)
        (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) :
      A)

Tactic:
rw [Finset.sum_comm] at key

Premises used: Finset.sum_comm
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
key :
  Eq (α := A)
    (∑ y_1 ∈ ℛx.index,
        ∑ x_1 ∈ ℛy.index,
          HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A)
            (ℛx.right y_1 * ℛy.right x_1) :
      A)
    ((algebraMap R A : (a : R) → A)
        (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) :
      A)
⊢ ∑ y_1 ∈ ℛx.index,
      ∑ x_1 ∈ ℛy.index,
        HMul.hMul (α := A) ((antipode R : (a : A) → A) (ℛx.left y_1 * ℛy.left x_1) : A) (ℛx.right y_1 * ℛy.right x_1) =
    HSMul.hSMul (β := A) (HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) y : R) ((counit : (a : A) → R) x : R)) 1

Tactic:
simpa [Algebra.algebraMap_eq_smul_one, mul_comm (counit x) (counit y)] using key

Premises used: CoalgebraStruct.counit, Algebra.algebraMap_eq_smul_one, mul_comm, DFunLike.coe
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
⊢ HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (LinearMap.mul' R A))
      (toConv
        (LinearMap.mul' R A ∘ₗ
          TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))) =
    1

Tactic:
WithConv.ext (TensorProduct.ext' fun x y => ?_)

Premises used: WithConv.ext, TensorProduct.ext'
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
refine_2 :
  ∀ (x y : A),
    Eq (α := A)
      (((HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (LinearMap.mul' R A))
                (toConv
                  (LinearMap.mul' R A ∘ₗ
                    TensorProduct.map (antipode R) (antipode R) ∘ₗ
                      (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)))).ofConv :
            (a : A ⊗[R] A) → A)
          (x ⊗ₜ[R] y) :
        A)
      ((ofConv 1 : (a : A ⊗[R] A) → A) (x ⊗ₜ[R] y) : A)
⊢ HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (LinearMap.mul' R A))
      (toConv
        (LinearMap.mul' R A ∘ₗ
          TensorProduct.map (antipode R) (antipode R) ∘ₗ (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A))) =
    1

Tactic:
refine WithConv.ext (TensorProduct.ext' fun x y => ?_)

Premises used: WithConv.ext, TensorProduct.ext'
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
refine_2 :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (LinearMap.mul' R A)
                (LinearMap.mul' R A ∘ₗ
                  TensorProduct.map (antipode R) (antipode R) ∘ₗ
                    (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            ((comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] (A ⊗[R] A)) (x ⊗ₜ[R] y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    (((HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (LinearMap.mul' R A))
              (toConv
                (LinearMap.mul' R A ∘ₗ
                  TensorProduct.map (antipode R) (antipode R) ∘ₗ
                    (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)))).ofConv :
          (a : A ⊗[R] A) → A)
        (x ⊗ₜ[R] y) :
      A)
    ((ofConv 1 : (a : A ⊗[R] A) → A) (x ⊗ₜ[R] y) : A)

Tactic:
simp only [LinearMap.convMul_apply, LinearMap.convOne_apply]

Premises used: LinearMap.convOne_apply, LinearMap.convMul_apply
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : A
refine_2 :
  Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (LinearMap.mul' R A)
                (LinearMap.mul' R A ∘ₗ
                  TensorProduct.map (antipode R) (antipode R) ∘ₗ
                    (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A A A :
                  A ⊗[R] A ⊗[R] (A ⊗[R] A) ≃ₗ[R] A ⊗[R] A ⊗[R] (A ⊗[R] A)) :
                (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A ⊗[R] (A ⊗[R] A))
              ((comul : (a : A) → A ⊗[R] A) x ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)
⊢ Eq (α := A)
    ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
        ((TensorProduct.map (LinearMap.mul' R A)
                (LinearMap.mul' R A ∘ₗ
                  TensorProduct.map (antipode R) (antipode R) ∘ₗ
                    (↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A)) :
              (a : A ⊗[R] A ⊗[R] (A ⊗[R] A)) → A ⊗[R] A)
            ((comul : (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] (A ⊗[R] A)) (x ⊗ₜ[R] y)) :
          A ⊗[R] A) :
      A)
    ((algebraMap R A : (a : R) → A) ((counit : (a : A ⊗[R] A) → R) (x ⊗ₜ[R] y) : R) : A)

Tactic:
rw [TensorProduct.comul_tmul]

Premises used: TensorProduct.comul_tmul