awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := S)
      (((((AlgebraTensorModule.curry (counit ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                    M →ₗ[S] R →ₗ[R] S) :
                  (a : M) → R →ₗ[R] S)
                x :
              R →ₗ[R] S) :
            (a : R) → S)
          1 :
        S)
      (((((AlgebraTensorModule.curry counit : M →ₗ[S] R →ₗ[R] S) : (a : M) → R →ₗ[R] S) x : R →ₗ[R] S) : (a : R) → S)
          1 :
        S)
⊢ Eq (α := M ⊗[R] R →ₗ[S] S) (counit ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) : M ⊗[R] R →ₗ[S] S)
    (counit : M ⊗[R] R →ₗ[S] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
⊢ Eq.{u_6 + 1} (α := S)
    (((((AlgebraTensorModule.curry (counit ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                  M →ₗ[S] R →ₗ[R] S) :
                (a : M) → R →ₗ[R] S)
              x :
            R →ₗ[R] S) :
          (a : R) → S)
        1 :
      S)
    (((((AlgebraTensorModule.curry counit : M →ₗ[S] R →ₗ[R] S) : (a : M) → R →ₗ[R] S) x : R →ₗ[R] S) : (a : R) → S) 1 :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
a :
  ∀ (x : M),
    Eq.{u_7 + 1} (α := M ⊗[S] M)
      (((((AlgebraTensorModule.curry
                    ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
                          (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
                        M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
                      (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R))) :
                  M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
                (a : M) → R →ₗ[R] M ⊗[S] M)
              x :
            LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
          (a : R) → M ⊗[S] M)
        1)
      (((((AlgebraTensorModule.curry (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                  M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
                (a : M) → R →ₗ[R] M ⊗[S] M)
              x :
            LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
          (a : R) → M ⊗[S] M)
        1)
⊢ Eq (α := M ⊗[R] R →ₗ[S] M ⊗[S] M)
    ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
            (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
          M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
        (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
      M ⊗[R] R →ₗ[S] M ⊗[S] M)
    (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) : M ⊗[R] R →ₗ[S] M ⊗[S] M)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
a :
  Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) (HSMul.hSMul.{u_5, u_7, u_7} (α := R) 1 x) : M ⊗[S] M)
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((((AlgebraTensorModule.curry
                  ((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
                        (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
                      M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) ∘ₗ
                    (comul : M ⊗[R] R →ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R))) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)
    (((((AlgebraTensorModule.curry (comul ∘ₗ (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)) :
                M →ₗ[S] LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
              (a : M) → R →ₗ[R] M ⊗[S] M)
            x :
          LinearMap.{u_5, u_5, u_5, u_7} (RingHom.id R) R (M ⊗[S] M)) :
        (a : R) → M ⊗[S] M)
      1)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
a :
  Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) x : M ⊗[S] M)
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) (HSMul.hSMul.{u_5, u_7, u_7} (α := R) 1 x) : M ⊗[S] M)

Tactic:
simp only [one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x : M
a :
  ∀ (x₁ x₂ : M),
    Eq.{u_7 + 1} (α := M ⊗[S] M)
      (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
                (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
              M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
            (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
          (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
                TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
              (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
            (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
        M ⊗[S] M)
      (x₁ ⊗ₜ[S] x₂ : M ⊗[S] M)
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          ((comul : (a : M) → M ⊗[S] M) x ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    ((comul : (a : M) → M ⊗[S] M) x : M ⊗[S] M)

Tactic:
hopf_tensor_induction comul (R := S) x with x₁ x₂

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S_1 : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S_1
inst_5 : Module R_1 A
inst_6 : Module S_1 A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S_1 A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Algebra R S
inst_12 : AddCommMonoid M
inst_13 : AddCommMonoid N
inst_14 : AddCommMonoid P
inst_15 : AddCommMonoid Q
inst_16 : Module R M
inst_17 : Module R N
inst_18 : Module R P
inst_19 : Module R Q
inst_20 : Module S M
inst_21 : IsScalarTower R S M
inst_22 : Coalgebra S M
inst_23 : Module S N
inst_24 : IsScalarTower R S N
inst_25 : Coalgebra S N
inst_26 : Coalgebra R P
inst_27 : Coalgebra R Q
x x₁ x₂ : M
⊢ Eq.{u_7 + 1} (α := M ⊗[S] M)
    (((_root_.TensorProduct.map (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M)
              (↑(AlgebraTensorModule.rid R S M) : M ⊗[R] R →ₗ[S] M) :
            M ⊗[R] R ⊗[S] (M ⊗[R] R) →ₗ[S] M ⊗[S] M) :
          (a : M ⊗[R] R ⊗[S] (M ⊗[R] R)) → M ⊗[S] M)
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S M M R R :
              TensorProduct.{u_5, u_7, u_5} R (M ⊗[S] M) (R ⊗[R] R) ≃ₗ[S] M ⊗[R] R ⊗[S] (M ⊗[R] R)) :
            (a : M ⊗[S] M ⊗[R] (R ⊗[R] R)) → M ⊗[R] R ⊗[S] (M ⊗[R] R))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (1 ⊗ₜ[R] 1))) :
      M ⊗[S] M)
    (x₁ ⊗ₜ[S] x₂ : M ⊗[S] M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Coalgebra S M
⊢ Eq (α := M ⊗[R] R ≃ₗ[S] M) (CoalgEquiv.toLinearEquiv (TensorProduct.rid R S M) : M ⊗[R] R ≃ₗ[S] M)
    (AlgebraTensorModule.rid R S M : M ⊗[R] R ≃ₗ[S] M)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, TensorProduct.AlgebraTensorModule.rid, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Coalgebra S M
r : R
a : M
⊢ (TensorProduct.rid R S M : (a : M ⊗[R] R) → M) (a ⊗ₜ[R] r) = r • a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_5
S : Type u_6
M : Type u_7
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Coalgebra S M
a : M
⊢ Eq (α := M ⊗[R] R) ((CoalgEquiv.symm (TensorProduct.rid R S M) : (a : M) → M ⊗[R] R) a : M ⊗[R] R)
    (a ⊗ₜ[R] 1 : M ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
simp :
  Eq (α := C →ₗ[R] R)
    (((↑(_root_.TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ AlgebraTensorModule.map ε ε :
        LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id R) (C ⊗[R] C) R) ∘ₗ
      (δ : C →ₗ[R] C ⊗[R] C))
    ε
⊢ Eq (α := C →ₗ[R] R) (counit ∘ₗ δ) ε

Tactic:
simp only [counit_def, AlgebraTensorModule.rid_eq_rid, ← lid_eq_rid]

Premises used: TensorProduct.AlgebraTensorModule.rid_eq_rid, TensorProduct.counit_def, TensorProduct.lid_eq_rid
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
⊢ Eq (α := C →ₗ[R] R) ((μ ∘ₗ map ε ε) ∘ₗ δ) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ)

Tactic:
simp [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
h : ∀ (x : C), Eq.{u_5 + 1} (α := R) (((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ : (a : C) → R) x : R) ((ε : (a : C) → R) x : R)
⊢ Eq (α := C →ₗ[R] R) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ) ε

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
x : C
⊢ Eq.{u_5 + 1} (α := R) (((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ : (a : C) → R) x : R) ((ε : (a : C) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
_ : Eq (α := C →ₗ[R] R) ((μ ∘ₗ map ε ε) ∘ₗ δ) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ)
_₁ : Eq (α := C →ₗ[R] R) ((μ ∘ₗ ε ▷ R) ∘ₗ C ◁ ε ∘ₗ δ) ε
⊢ Eq (α := C →ₗ[R] R)
    (((↑(_root_.TensorProduct.lid R R) : R ⊗[R] R →ₗ[R] R) ∘ₗ AlgebraTensorModule.map ε ε :
        LinearMap.{u_5, u_5, u_6, u_5} (RingHom.id R) (C ⊗[R] C) R) ∘ₗ
      (δ : C →ₗ[R] C ⊗[R] C))
    ε

Tactic:
calc
        (μ ∘ₗ (ε ⊗ₘ ε)) ∘ₗ δ
    _ = (μ ∘ₗ ε ▷ R) ∘ₗ (C ◁ ε ∘ₗ δ) := by simp [coassoc_simps]
    _ = ε := by ext; simp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R_1 : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R_1 S
inst_5 : Module R_1 A
inst_6 : Module S A
inst_7 : Module R_1 B
inst_8 : IsScalarTower R_1 S A
R : Type u_5
C : Type u_6
inst_9 : CommSemiring R
inst_10 : AddCommMonoid C
inst_11 : Module R C
inst_12 : Coalgebra R C
inst_13 : IsCocomm R C
⊢ Eq.{u_6 + 1} (α := C →ₗ[R] C ⊗[R] C ⊗[R] (C ⊗[R] C)) (map δ δ ∘ₗ δ) (δ ∘ₗ δ)

Tactic:
simp [comul_def, coassoc_simps]

Premises used: TensorProduct.comul_def
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
a :
  ∀ (i j : Fin 2),
    Eq (α := ℝ) ((leftMulMatrix basisOneI : (a : ℂ) → Matrix (Fin 2) (Fin 2) ℝ) z i j : ℝ)
      (!![z.re, -z.im; z.im, z.re] i j : ℝ)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((leftMulMatrix basisOneI : (a : ℂ) → Matrix (Fin 2) (Fin 2) ℝ) z : Matrix (Fin 2) (Fin 2) ℝ)
    (!![z.re, -z.im; z.im, z.re] : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
i j : Fin 2
a :
  ![z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  ![z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re -
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im,
        z.re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im +
          z.im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j

Tactic:
fin_cases j
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
i : Fin 2
a : ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0
⊢ ![z.re * re 1 - z.im * im 1, z.re * im 1 + z.im * re 1] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Tactic:
simp only [one_re, mul_one, one_im, mul_zero,
      sub_zero, zero_add]

Premises used: sub_zero, zero_add, MulZeroClass.mul_zero, mul_one, Complex.one_re, Complex.one_im
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
i : Fin 2
a :
  ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 0
a₁ :
  ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 0
⊢ ![z.re, z.im] i = ![![z.re, -z.im], ![z.im, z.re]] i 0

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ ![z.re, z.im] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
i : Fin 2
a : ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1
⊢ ![z.re * I.re - z.im * I.im, z.re * I.im + z.im * I.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1

Tactic:
simp only [I_re, mul_zero, I_im,
      mul_one, zero_sub, add_zero]

Premises used: Complex.I_re, Complex.I_im, MulZeroClass.mul_zero, mul_one, add_zero, zero_sub
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
i : Fin 2
a :
  ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1
a₁ :
  ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1
⊢ ![-z.im, z.re] i = ![![z.re, -z.im], ![z.im, z.re]] i 1

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ ![-z.im, z.re] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    ![![z.re, -z.im], ![z.im, z.re]] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
rw : HAdd.hAdd (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) = 2 * z.re
⊢ (trace ℝ ℂ : (a : ℂ) → ℝ) z = 2 * z.re

Tactic:
rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex,
    Matrix.trace_fin_two]

Premises used: Matrix.trace_fin_two, Algebra.leftMulMatrix_complex, Algebra.trace_eq_matrix_trace, Complex.basisOneI
-- Module: Mathlib.RingTheory.Complex
Goal:
z : ℂ
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (!![z.re, -z.im; z.im, z.re] 0 0 : ℝ) (!![z.re, -z.im; z.im, z.re] 1 1 : ℝ) = 2 * z.re

Tactic:
(two_mul _).symm

Premises used: Eq.mpr, Fin.cons, two_mul, Fin.induction.go, Fin.ofNat, Fin.induction, Fin.cases, Eq.symm, Matrix.vecCons