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 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 (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))
            ((∑ 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 (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)

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_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))
              ((∑ 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 (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)

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_2 :
  Eq (α := A)
    (∑ x_1 ∈ ℛy.index,
        ∑ x_2 ∈ ℛx.index,
          HMul.hMul (β := A) (ℛx.left x_2 * ℛy.left x_1)
            ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
                ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                      (ℛx.right x_2 ⊗ₜ[R] ℛy.right x_1)) :
                  A ⊗[R] A) :
              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)
            (((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_2 :
  Eq (α := A)
    (∑ y_1 ∈ ℛx.index,
        ∑ x_1 ∈ ℛy.index,
          HMul.hMul (β := A) (ℛx.left y_1 * ℛy.left x_1)
            ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
                ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                      (ℛx.right y_1 ⊗ₜ[R] ℛy.right x_1)) :
                  A ⊗[R] A) :
              A) :
      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) (ℛx.left x_2 * ℛy.left x_1)
            ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
                ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                      (ℛx.right x_2 ⊗ₜ[R] ℛy.right x_1)) :
                  A ⊗[R] A) :
              A) :
      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_2 :
  ∑ y_1 ∈ ℛx.index,
      ∑ x_1 ∈ ℛy.index,
        HMul.hMul (β := A) (ℛx.left y_1 * ℛy.left x_1)
          ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
              ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                  (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (ℛx.right y_1 ⊗ₜ[R] ℛy.right x_1)) :
                A ⊗[R] A) :
            A) =
    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) (ℛx.left y_1 * ℛy.left x_1)
            ((LinearMap.mul' R A : (a : A ⊗[R] A) → A)
                ((TensorProduct.map (antipode R) (antipode R) : (a : A ⊗[R] A) → A ⊗[R] A)
                    (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) : (a : A ⊗[R] A) → A ⊗[R] A)
                      (ℛx.right y_1 ⊗ₜ[R] ℛy.right x_1)) :
                  A ⊗[R] A) :
              A) :
      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)
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i * ℛy.left j *
          HMul.hMul (α := A) (β := A) ((antipode R : (a : A) → A) (ℛy.right j) : A)
            ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i *
          HMul.hMul (β := A) (HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A))
            ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- 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)
    (∑ i ∈ ℛx.index,
      ∑ j ∈ ℛy.index,
        ℛx.left i *
          HMul.hMul (β := A) (HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A))
            ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A)
          (∑ j ∈ ℛy.index, HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
simp [Finset.sum_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, 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
rw rw₁ :
  Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
⊢ Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A)
          (∑ j ∈ ℛy.index, HMul.hMul (β := A) (ℛy.left j) ((antipode R : (a : A) → A) (ℛy.right j) : A) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
rw [sum_mul_antipode_eq_smul ℛy]

Premises used: HopfAlgebra.sum_mul_antipode_eq_smul
-- 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)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (β := A) (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) y : R) 1)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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
e_f :
  Eq.{v + 1} (α := ℛx.ι → A)
    (fun (i : ℛx.ι) ↦
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    fun (i : ℛx.ι) ↦
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A))
⊢ Eq (α := A)
    (∑ i ∈ ℛx.index,
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    (∑ i ∈ ℛx.index,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A)))

Tactic:
congr 1
-- 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
e_f :
  ∀ (i : ℛx.ι),
    ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A) =
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A))
⊢ Eq.{v + 1} (α := ℛx.ι → A)
    (fun (i : ℛx.ι) ↦
      ℛx.left i *
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
          ((antipode R : (a : A) → A) (ℛx.right i) : A))
    fun (i : ℛx.ι) ↦
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
ext i
-- 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
i : ℛx.ι
e_f :
  HMul.hMul (β := A)
      (HMul.hMul (β := A) (ℛx.left i) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A))
      ((antipode R : (a : A) → A) (ℛx.right i) : A) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A))
e_f₁ :
  HMul.hMul (β := A)
      (HMul.hMul (β := A) (ℛx.left i) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A))
      ((antipode R : (a : A) → A) (ℛx.right i) : A) =
    HMul.hMul (β := A)
      (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A) (ℛx.left i))
      ((antipode R : (a : A) → A) (ℛx.right i) : A)
e_f₂ e_f₃ :
  HMul.hMul (β := A)
      (HMul.hMul (β := A) (ℛx.left i) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A))
      ((antipode R : (a : A) → A) (ℛx.right i) : A) =
    HMul.hMul (β := A)
      (HMul.hMul (β := A) (ℛx.left i) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A))
      ((antipode R : (a : A) → A) (ℛx.right i) : A)
⊢ ℛx.left i *
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        ((antipode R : (a : A) → A) (ℛx.right i) : A) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A))

Tactic:
rw [← mul_assoc, ← mul_assoc, Algebra.commutes]

Premises used: mul_assoc, Algebra.commutes
-- 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 rw₁ :
  HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A)
⊢ ∑ i ∈ ℛx.index,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
        (HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A)) =
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A)

Tactic:
rw [← Finset.mul_sum]

Premises used: Finset.mul_sum
-- 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 rw₁ :
  HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1)
⊢ HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (∑ i ∈ ℛx.index, HMul.hMul (β := A) (ℛx.left i) ((antipode R : (a : A) → A) (ℛx.right i) : A) : A) =
    HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1)

Tactic:
rw [sum_mul_antipode_eq_smul ℛx]

Premises used: HopfAlgebra.sum_mul_antipode_eq_smul
-- 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
⊢ HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((counit : (a : A) → R) y : R) : A)
      (HSMul.hSMul.{u, v, v} (α := R) (β := A) ((counit : (a : A) → R) x : R) 1) =
    HSMul.hSMul (β := A) (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) 1

Tactic:
simp only [Algebra.smul_def, mul_one, ← map_mul, mul_comm (counit x)]

Premises used: CoalgebraStruct.counit, map_mul, mul_comm, Algebra.smul_def, mul_one, 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 x y : A
ℛx : Coalgebra.Repr R x := ℛ R x
ℛy : Coalgebra.Repr R y := ℛ R y
⊢ HSMul.hSMul (β := A) (HMul.hMul (α := R) (β := R) ((counit : (a : A) → R) x : R) ((counit : (a : A) → R) y : R)) 1 =
    HSMul.hSMul (β := A) (HSMul.hSMul (α := R) (β := R) ((counit : (a : A) → R) y : R) ((counit : (a : A) → R) x : R)) 1

Tactic:
simp only [smul_eq_mul, mul_comm (counit y)]

Premises used: CoalgebraStruct.counit, mul_comm, smul_eq_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R) ((LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul : (a : R) → R) 1 : R)
    ((Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit : (a : R) → R) 1 : R)
⊢ Eq (α := R →ₗ[R] R) (LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul)
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R) ((LinearMap.mul' R R ∘ₗ LinearMap.rTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul : (a : R) → R) 1 : R)
    ((Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit : (a : R) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
h :
  Eq (α := R) ((LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul : (a : R) → R) 1 : R)
    ((Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit : (a : R) → R) 1 : R)
⊢ Eq (α := R →ₗ[R] R) (LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul)
    (Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit)

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R) ((LinearMap.mul' R R ∘ₗ LinearMap.lTensor R LinearMap.id ∘ₗ CoalgebraStruct.comul : (a : R) → R) 1 : R)
    ((Algebra.linearMap R R ∘ₗ CoalgebraStruct.counit : (a : R) → R) 1 : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.HopfAlgebra.Basic
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₗ[R] R) (antipode R) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ HMul.hMul (α := A) ((antipode R : (a : A) → A) a : A) a = 1

Tactic:
simpa [ha, -mul_antipode_lTensor_comul_apply] using mul_antipode_rTensor_comul_apply (R := R) a

Premises used: HopfAlgebra.mul_antipode_rTensor_comul_apply, HopfAlgebra.mul_antipode_lTensor_comul_apply
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ HMul.hMul (β := A) a ((antipode R : (a : A) → A) a : A) = 1

Tactic:
simpa [ha, -mul_antipode_lTensor_comul_apply] using mul_antipode_lTensor_comul_apply (R := R) a

Premises used: HopfAlgebra.mul_antipode_lTensor_comul_apply
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
huv :
  Eq.{u_2 + 1} (α := A)
    ((↑{ val := (↑1 : A), inv := (antipode R : (a : A) → A) (↑1 : A), val_inv := ⋯, inv_val := ⋯ } : A) : A)
    ((↑1 : A) : A)
⊢ Eq.{u_2 + 1} (α := Aˣ)
    ({ val := (↑1 : A), inv := (antipode R : (a : A) → A) (↑1 : A), val_inv := ⋯, inv_val := ⋯ } : Aˣ) (1 : Aˣ)

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : A
⊢ Eq.{u_2 + 1} (α := A)
    ((↑{ val := (↑1 : A), inv := (antipode R : (a : A) → A) (↑1 : A), val_inv := ⋯, inv_val := ⋯ } : A) : A)
    ((↑1 : A) : A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a_1 b_1 : A
a b : GroupLike R A
huv :
  (↑{ val := (↑(a * b) : A), inv := (antipode R : (a : A) → A) (↑(a * b) : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } : A) =
    (↑({ val := (↑a : A), inv := (antipode R : (a : A) → A) (↑a : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } *
          { val := (↑b : A), inv := (antipode R : (a : A) → A) (↑b : A), val_inv := ⋯, inv_val := ⋯ : Aˣ }) :
      A)
⊢ { val := (↑(a * b) : A), inv := (antipode R : (a : A) → A) (↑(a * b) : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } =
    { val := (↑a : A), inv := (antipode R : (a : A) → A) (↑a : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } *
      { val := (↑b : A), inv := (antipode R : (a : A) → A) (↑b : A), val_inv := ⋯, inv_val := ⋯ : Aˣ }

Tactic:
ext
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a_1 b_1 : A
a b : GroupLike R A
⊢ (↑{ val := (↑(a * b) : A), inv := (antipode R : (a : A) → A) (↑(a * b) : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } : A) =
    (↑({ val := (↑a : A), inv := (antipode R : (a : A) → A) (↑a : A), val_inv := ⋯, inv_val := ⋯ : Aˣ } *
          { val := (↑b : A), inv := (antipode R : (a : A) → A) (↑b : A), val_inv := ⋯, inv_val := ⋯ : Aˣ }) :
      A)

Tactic:
rfl
-- Module: Mathlib.RingTheory.HopfAlgebra.GroupLike
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ IsUnit a

Tactic:
(GroupLike.toUnits R ⟨a, ha⟩).isUnit

Premises used: GroupLike.toUnits, GroupLike.mk, Units.isUnit, DFunLike.coe