awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b : 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)
have 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))
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))
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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))
have refine_1 : HMul.hMul (α := WithConv (A ⊗[R] A →ₗ[R] A)) (toConv (antipode R ∘ₗ LinearMap.mul' R A)) (toConv (LinearMap.mul' R A)) =
  1
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))
      ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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
⊢ 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))
have 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
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))
      ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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
have 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)
Tactic: refine WithConv.ext (TensorProduct.ext' fun x y => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b 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)
have 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)
Tactic: simp only [LinearMap.convMul_apply, LinearMap.convOne_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : 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)
have 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)
Tactic: rw [TensorProduct.comul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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
| ((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)
have 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)
Tactic: rw [← ℛx.eq, ← ℛy.eq]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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)
        ((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)
have 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)
Tactic: conv_lhs => rw [← ℛx.eq, ← ℛy.eq]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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)
        ((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)
have 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)
Tactic: simp only [TensorProduct.sum_tmul, TensorProduct.tmul_sum, map_sum,
      TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_tmul, TensorProduct.map_tmul,
      LinearMap.mul'_apply, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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)
    (∑ 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)
have 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)
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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)
    (∑ 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)
have 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
Tactic: simp only [TensorProduct.counit_tmul, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (hypothesis)
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
⊢ ∑ 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
have 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)
Tactic: have key := mul_antipode_rTensor_comul_apply (R := R) (x * y)
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (hypothesis)
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)
⊢ ∑ 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
have 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)
Tactic: rw [Bialgebra.comul_mul, ← ℛx.eq, ← ℛy.eq] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (hypothesis)
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)
⊢ ∑ 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
have 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)
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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (hypothesis)
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)
⊢ ∑ 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
have 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)
Tactic: rw [Finset.sum_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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
have 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)
Tactic: refine WithConv.ext (TensorProduct.ext' fun x y => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b 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)
have 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)
Tactic: simp only [LinearMap.convMul_apply, LinearMap.convOne_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : HopfAlgebra R A
a b x y : 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)
have 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)
Tactic: rw [TensorProduct.comul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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
| ((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)
have 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)
Tactic: rw [← ℛx.eq, ← ℛy.eq]
-- Lean 4 proof step from Mathlib.RingTheory.HopfAlgebra.Basic (goal)
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)
        ((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)
have 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)
Tactic: conv_lhs => rw [← ℛx.eq, ← ℛy.eq]