awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
f g : A →ₗc[R] R
x : A
hf : Eq.{u + 1} (α := R) ((counit : (a : R) → R) ((f : (a : A) → R) x : R) : R) ((counit : (a : A) → R) x : R)
hg : Eq.{u + 1} (α := R) ((counit : (a : R) → R) ((g : (a : A) → R) x : R) : R) ((counit : (a : A) → R) x : R)
⊢ Eq.{u + 1} (α := R) ((f : (a : A) → R) x : R) ((g : (a : A) → R) x : R)

Tactic:
simp_all only [CommSemiring.counit_apply]

Premises used: CommSemiring.counit_apply
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
f g : A →ₗc[R] R
⊢ f = g

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
a : A
repr : Repr.{u, v, u_2} R a
F : Type u_1
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
φ : F
rw :
  Eq.{w + 1} (α := B ⊗[R] B)
    (∑ x ∈ repr.index,
      ((map (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
              (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u, u, v, w} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
          (a : A ⊗[R] A) → B ⊗[R] B)
        (repr.left x ⊗ₜ[R] repr.right x))
    (∑ i ∈ repr.index, ((⇑φ : (a : A) → B) ∘ repr.left) i ⊗ₜ[R] ((⇑φ : (a : A) → B) ∘ repr.right) i)
⊢ Eq.{w + 1} (α := B ⊗[R] B)
    (((map (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
                (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
              comul :
            LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) :
          (a : A) → B ⊗[R] B)
        a :
      B ⊗[R] B)
    (∑ i ∈ repr.index, ((⇑φ : (a : A) → B) ∘ repr.left) i ⊗ₜ[R] ((⇑φ : (a : A) → B) ∘ repr.right) i : B ⊗[R] B)

Tactic:
rw [LinearMap.comp_apply, ← repr.eq, map_sum]

Premises used: LinearMap.comp_apply, map_sum, Coalgebra.Repr.eq
-- Module: Mathlib.RingTheory.Coalgebra.Hom
Goal:
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : AddCommMonoid B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : Coalgebra R A
inst_6 : Coalgebra R B
a : A
repr : Repr.{u, v, u_2} R a
F : Type u_1
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
φ : F
⊢ Eq.{w + 1} (α := B ⊗[R] B)
    (∑ x ∈ repr.index,
      ((map (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
              (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
            LinearMap.{u, u, v, w} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
          (a : A ⊗[R] A) → B ⊗[R] B)
        (repr.left x ⊗ₜ[R] repr.right x))
    (∑ i ∈ repr.index, ((⇑φ : (a : A) → B) ∘ repr.left) i ⊗ₜ[R] ((⇑φ : (a : A) → B) ∘ repr.right) i)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
X : Type u_3
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : IsCocomm R A
⊢ IsCocomm R A[X]

Tactic:
Finsupp.instIsCocomm R X A

Premises used: Finsupp.instIsCocomm, MonoidAlgebra
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
X : Type u_3
inst_2 : Module R A
inst_3 : Coalgebra R A
x : X
a : A
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : A[X]) → R) (single x a) : R) ((counit : (a : A) → R) a : R)

Tactic:
Finsupp.counit_single _ _ _ _ _

Premises used: Finsupp.counit_single
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
X : Type u_3
inst_2 : Module R A
inst_3 : Coalgebra R A
x : X
a : A
⊢ Eq (α := TensorProduct R A[X] A[X])
    ((comul : (a : A[X]) → TensorProduct R A[X] A[X]) (single x a) : TensorProduct R A[X] A[X])
    ((TensorProduct.map (lsingle x) (lsingle x) : (a : TensorProduct R A A) → TensorProduct R A[X] A[X])
        ((comul : (a : A) → TensorProduct R A A) a) :
      TensorProduct R A[X] A[X])

Tactic:
Finsupp.comul_single _ _ _ _ _

Premises used: Finsupp.comul_single, MonoidAlgebra
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : IsCocomm R A
⊢ IsCocomm.{u_1, u_2} R A[T;T⁻¹]

Tactic:
inferInstanceAs <| IsCocomm R A[ℤ]

Premises used: _private.0.LaurentPolynomial.instIsCocomm._proof_1
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq (α := TensorProduct R A[T;T⁻¹] A[T;T⁻¹])
    ((comul : (a : A[T;T⁻¹]) → TensorProduct R A[T;T⁻¹] A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) a) :
      TensorProduct R A[T;T⁻¹] A[T;T⁻¹])
    ((TensorProduct.map (lsingle 0) (lsingle 0) : (a : TensorProduct R A A) → TensorProduct R A[ℤ] A[ℤ])
        ((comul : (a : A) → TensorProduct R A A) a) :
      TensorProduct R A[ℤ] A[ℤ])

Tactic:
comul_single _ _

Premises used: AddMonoidAlgebra.comul_single, Finsupp.single
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
n : ℤ
⊢ Eq (α := TensorProduct R A[ℤ] A[ℤ])
    ((comul : (a : A[ℤ]) → TensorProduct R A[ℤ] A[ℤ])
        (HMul.hMul (α := A[T;T⁻¹]) (β := A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) a : A[T;T⁻¹]) (T n)) :
      TensorProduct R A[ℤ] A[ℤ])
    ((TensorProduct.map (lsingle n) (lsingle n) : (a : TensorProduct R A A) → TensorProduct R A[ℤ] A[ℤ])
        ((comul : (a : A) → TensorProduct R A A) a) :
      TensorProduct R A[ℤ] A[ℤ])

Tactic:
simp [← single_eq_C_mul_T]

Premises used: LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
a : R
n : ℤ
⊢ Eq (α := TensorProduct R R[T;T⁻¹] R[T;T⁻¹])
    ((comul : (a : R[T;T⁻¹]) → TensorProduct R R[T;T⁻¹] R[T;T⁻¹])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)) :
      TensorProduct R R[T;T⁻¹] R[T;T⁻¹])
    (T n ⊗ₜ[R] HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n) :
      TensorProduct R R[T;T⁻¹] R[T;T⁻¹])

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : A[T;T⁻¹]) → R) ((C : (a : A) → A[T;T⁻¹]) a : A[T;T⁻¹]) : R)
    ((counit : (a : A) → R) a : R)

Tactic:
counit_single _ _

Premises used: AddMonoidAlgebra.counit_single, Finsupp.single
-- Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : A
n : ℤ
⊢ Eq.{u_1 + 1} (α := R)
    ((counit : (a : A[T;T⁻¹]) → R)
        (HMul.hMul (α := A[T;T⁻¹]) (β := A[T;T⁻¹]) ((C : (a : A) → A[T;T⁻¹]) a : A[T;T⁻¹]) (T n)) :
      R)
    ((counit : (a : A) → R) a : R)

Tactic:
simp [← single_eq_C_mul_T]

Premises used: LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
⊢ Eq.{u_2 + 1} (α := Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) comul
    (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
      comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) Aᵐᵒᵖ R) counit
    (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
rw :
  Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    (((↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) ∘ₗ
            (rTensor Aᵐᵒᵖ (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ
              (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
            map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
⊢ Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    (((↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) ∘ₗ
            rTensor Aᵐᵒᵖ comul ∘ₗ comul :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ comul ∘ₗ comul : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) x : Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))

Tactic:
rw [comul_def, rTensor_comp, rTensor_comp]

Premises used: LinearMap.rTensor_comp, MulOpposite.comul_def
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
simp :
  Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ : (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((map (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) LinearMap.id :
            (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
          ((map comul LinearMap.id : (a : A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
            ((map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) LinearMap.id :
                (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → A ⊗[R] Aᵐᵒᵖ)
              ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
                  (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
                ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))))) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
            ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
⊢ Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    (((↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) ∘ₗ
            (rTensor Aᵐᵒᵖ (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ
              (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
            map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))

Tactic:
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_map, rTensor_def]

Premises used: LinearMap.coe_comp, LinearMap.rTensor_def, Function.comp_apply, LinearMap.lTensor_map, LinearEquiv.coe_coe
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
simp_rw :
  Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ (lTensor Aᵐᵒᵖ LinearMap.id ∘ₗ rTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
            rTensor (A ⊗[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] (A ⊗[R] Aᵐᵒᵖ)) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((TensorProduct.assoc R A A Aᵐᵒᵖ : (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] (A ⊗[R] Aᵐᵒᵖ))
          ((lTensor (A ⊗[R] A) (LinearMap.id ∘ₗ LinearMap.id ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                rTensor A
                  (comul ∘ₗ
                    (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
              (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
            ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ
              ((lTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                comul ∘ₗ
                  (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
            rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
⊢ Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ : (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((map (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) LinearMap.id :
            (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
          ((map comul LinearMap.id : (a : A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
            ((map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) LinearMap.id :
                (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → A ⊗[R] Aᵐᵒᵖ)
              ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
                  (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
                ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))))) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
            ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))

Tactic:
simp_rw [← map_map_assoc, map_map, comp_assoc, ← lTensor_comp_rTensor]

Premises used: TensorProduct.map_map, LinearMap.comp_assoc, LinearMap.lTensor_comp_rTensor, TensorProduct.map_map_assoc
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ (lTensor Aᵐᵒᵖ LinearMap.id ∘ₗ rTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
            rTensor (A ⊗[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] (A ⊗[R] Aᵐᵒᵖ)) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((TensorProduct.assoc R A A Aᵐᵒᵖ : (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] (A ⊗[R] Aᵐᵒᵖ))
          ((lTensor (A ⊗[R] A) (LinearMap.id ∘ₗ LinearMap.id ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                rTensor A
                  (comul ∘ₗ
                    (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
              (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
            ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ
              ((lTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                comul ∘ₗ
                  (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
            rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))

Tactic:
simp [lTensor_tensor, comp_assoc]

Premises used: LinearMap.comp_assoc, LinearMap.lTensor_tensor
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
simp :
  Eq (α := TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    ((map (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ))
            (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] A) → R ⊗[R] Aᵐᵒᵖ)
        ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    (((TensorProduct.mk R R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ →ₗ[R] R ⊗[R] Aᵐᵒᵖ) 1 : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
⊢ Eq (α := TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    ((rTensor Aᵐᵒᵖ counit ∘ₗ comul : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x : TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    (((TensorProduct.mk R R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ →ₗ[R] R ⊗[R] Aᵐᵒᵖ) 1 : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)

Tactic:
simp only [counit_def, comul_def, coe_comp, Function.comp_apply, rTensor_map, comp_assoc]

Premises used: LinearMap.comp_assoc, MulOpposite.counit_def, LinearMap.coe_comp, LinearMap.rTensor_map, Function.comp_apply, MulOpposite.comul_def
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    ((map (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ))
            (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
          (a : A ⊗[R] A) → R ⊗[R] Aᵐᵒᵖ)
        ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    (((TensorProduct.mk R R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ →ₗ[R] R ⊗[R] Aᵐᵒᵖ) 1 : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)

Tactic:
simp [← lTensor_comp_rTensor]

Premises used: LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
simp :
  Eq (α := TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
            (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] R)
        ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    (((LinearMap.flip (TensorProduct.mk R Aᵐᵒᵖ R) : (a : R) → Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] R) 1 : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
⊢ Eq (α := TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    ((lTensor Aᵐᵒᵖ counit ∘ₗ comul : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x : TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    (((LinearMap.flip (TensorProduct.mk R Aᵐᵒᵖ R) : (a : R) → Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] R) 1 : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)

Tactic:
simp only [counit_def, comul_def, coe_comp, Function.comp_apply, lTensor_map, comp_assoc]

Premises used: LinearMap.comp_assoc, MulOpposite.counit_def, LinearMap.coe_comp, Function.comp_apply, MulOpposite.comul_def, LinearMap.lTensor_map
-- Module: Mathlib.RingTheory.Coalgebra.MulOpposite
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
            (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] R)
        ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    (((LinearMap.flip (TensorProduct.mk R Aᵐᵒᵖ R) : (a : R) → Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] R) 1 : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)

Tactic:
simp [← rTensor_comp_lTensor]

Premises used: LinearMap.rTensor_comp_lTensor
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : CoalgebraStruct R B
inst_10 : CoalgebraStruct S A
⊢ Eq (α := A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) (comul : A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (((↑(AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
          TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
        (AlgebraTensorModule.map comul comul : A ⊗[R] B →ₗ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
      A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : CoalgebraStruct R B
inst_10 : CoalgebraStruct S A
⊢ Eq (α := A ⊗[R] B →ₗ[S] S) (counit : A ⊗[R] B →ₗ[S] S)
    (((↑(AlgebraTensorModule.rid R S S) : S ⊗[R] R →ₗ[S] S) : S ⊗[R] R →ₗ[S] S) ∘ₗ
        (AlgebraTensorModule.map counit counit : A ⊗[R] B →ₗ[S] S ⊗[R] R) :
      A ⊗[R] B →ₗ[S] S)

Tactic:
rfl

Premises used: rfl