awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
this : (i : n) → (x : A i) → Decidable (x ≠ 0)
⊢ Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        (x.sum (β := A) (DFinsupp.single (β := A))) :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
          (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        (x.sum (β := A) (DFinsupp.single (β := A))) :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))

Tactic:
aesop (add simp [map_map, DFinsupp.single_eq_pi_single])

Premises used: TensorProduct.map_map, DFinsupp.single_eq_pi_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
⊢ Eq (α := ((a : n) → A a) ⊗[R] ((a : n) → A a))
    ((comul : (a : (a : n) → A a) → ((a : n) → A a) ⊗[R] ((a : n) → A a)) (⇑x : (a : n) → A a) :
      ((a : n) → A a) ⊗[R] ((a : n) → A a))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) :
          (a : (Π₀ (i : n), A i) ⊗[R] Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        ((comul : (a : Π₀ (i : n), A i) → (Π₀ (i : n), A i) ⊗[R] Π₀ (i : n), A i) x) :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))

Tactic:
congr($comul_comp_dFinsuppCoeFnLinearMap x)

Premises used: Pi.comul_comp_dFinsuppCoeFnLinearMap, congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
apply :
  ∀ (x : n →₀ M),
    Eq.{u_1 + 1} (α := R) ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) x : R) ((counit : (a : n →₀ M) → R) x : R)
⊢ Eq (α := (n →₀ M) →ₗ[R] R) (counit ∘ₗ Finsupp.lcoeFun) counit

Tactic:
apply LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
rw :
  Eq.{u_1 + 1} (α := R)
    ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)
    ((counit : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)
⊢ Eq.{u_1 + 1} (α := R) ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) x : R) ((counit : (a : n →₀ M) → R) x : R)

Tactic:
rw [← Finsupp.univ_sum_single x]

Premises used: Finsupp.univ_sum_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq.{u_1 + 1} (α := R)
    ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)
    ((counit : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)

Tactic:
simp [-Finsupp.univ_sum_single, Finsupp.lcoeFun, Finsupp.single_eq_pi_single]

Premises used: Finsupp.univ_sum_single, Finsupp.lcoeFun, Finsupp.single_eq_pi_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : (a : n) → M) → R) (⇑x : (a : n) → M) : R) ((counit : (a : n →₀ M) → R) x : R)

Tactic:
congr($counit_comp_finsuppLcoeFun x)

Premises used: Pi.counit_comp_finsuppLcoeFun, congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
apply :
  ∀ (x : n →₀ M),
    Eq (α := (n → M) ⊗[R] (n → M)) ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
      ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
⊢ Eq (α := (n →₀ M) →ₗ[R] (n → M) ⊗[R] (n → M)) (comul ∘ₗ lcoeFun) (map lcoeFun lcoeFun ∘ₗ comul)

Tactic:
apply LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
rw :
  Eq (α := (n → M) ⊗[R] (n → M))
    ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))
    ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M))
      (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))
⊢ Eq (α := (n → M) ⊗[R] (n → M)) ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
    ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))

Tactic:
rw [← Finsupp.univ_sum_single x]

Premises used: Finsupp.univ_sum_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq (α := (n → M) ⊗[R] (n → M))
    ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))
    ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M))
      (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))

Tactic:
simp [-univ_sum_single, single_eq_pi_single, map_map]

Premises used: TensorProduct.map_map, Finsupp.univ_sum_single, Finsupp.single_eq_pi_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq (α := ((a : n) → M) ⊗[R] ((a : n) → M))
    ((comul : (a : (a : n) → M) → ((a : n) → M) ⊗[R] ((a : n) → M)) (⇑x : (a : n) → M))
    ((map lcoeFun lcoeFun : (a : (n →₀ M) ⊗[R] (n →₀ M)) → (n → M) ⊗[R] (n → M))
      ((comul : (a : n →₀ M) → (n →₀ M) ⊗[R] (n →₀ M)) x))

Tactic:
congr($comul_comp_finsuppLcoeFun x)

Premises used: congrArg, id, DFunLike.coe, Pi.comul_comp_finsuppLcoeFun
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
h :
  ∀ (i : n),
    Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i)))
      (((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) :
            ((i : n) → A i) ⊗[R] ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R]
              ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i))) ∘ₗ
          rTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ
        LinearMap.single R A i)
      ((lTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ LinearMap.single R A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i)))
    ((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) :
        ((i : n) → A i) ⊗[R] ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R]
          ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i))) ∘ₗ
      rTensor ((i : n) → A i) comul ∘ₗ comul)
    (lTensor ((i : n) → A i) comul ∘ₗ comul)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
h :
  ∀ (i : n),
    Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
      ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
        LinearMap.single R A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
h :
  ∀ (i : n),
    Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
      ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
          1 ∘ₗ
        LinearMap.single R A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
inst_6 : ∀ (i : n), IsCocomm.{u_1, u_3} R (A i)
h :
  ∀ (i : n) (x : A i),
    Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
      ((((↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) :
                  ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i)) ∘ₗ
                comul) ∘ₗ
              LinearMap.single R A i :
            (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
          x :
        ((i : n) → A i) ⊗[R] ((i : n) → A i))
      ((comul ∘ₗ LinearMap.single R A i : (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
        ((i : n) → A i) ⊗[R] ((i : n) → A i))
⊢ Eq (α := ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) :
        ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i)) ∘ₗ
      comul)
    comul

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
inst_6 : ∀ (i : n), IsCocomm.{u_1, u_3} R (A i)
i : n
x : A i
⊢ Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((((↑(TensorProduct.comm R ((i : n) → A i) ((i : n) → A i)) :
                ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i)) ∘ₗ
              comul) ∘ₗ
            LinearMap.single R A i :
          (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ LinearMap.single R A i : (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))

Tactic:
simp [← map_comm]

Premises used: TensorProduct.map_comm
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
h :
  ∀ (x : A),
    Eq (α := A ⊗[R] (A ⊗[R] A))
      (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ
              LinearMap.rTensor A comul ∘ₗ comul :
            (a : A) → A ⊗[R] (A ⊗[R] A))
          x :
        A ⊗[R] (A ⊗[R] A))
      ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x : A ⊗[R] (A ⊗[R] A))
⊢ Eq (α := A →ₗ[R] A ⊗[R] (A ⊗[R] A))
    ((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul)
    (LinearMap.lTensor A comul ∘ₗ comul)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
h :
  Eq.{u_3 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ
              LinearMap.rTensor A comul ∘ₗ comul :
            (a : A) → A ⊗[R] (A ⊗[R] A))
          x) :
      B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x) :
      B ⊗[R] (B ⊗[R] B))
⊢ Eq (α := A ⊗[R] (A ⊗[R] A))
    (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul :
          (a : A) → A ⊗[R] (A ⊗[R] A))
        x :
      A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x : A ⊗[R] (A ⊗[R] A))

Tactic:
apply (TensorProduct.map_bijective (e.linearEquiv R).bijective <|
        TensorProduct.map_bijective (e.linearEquiv R).bijective
        (e.linearEquiv R).bijective).injective

Premises used: LinearEquiv.bijective, Equiv.linearEquiv, Function.Bijective.injective, TensorProduct.map_bijective
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
h :
  Eq (α := B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.assoc R B B B : (a : B ⊗[R] B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
        ((TensorProduct.map
              ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A))
              LinearMap.id :
            (a : B ⊗[R] B) → B ⊗[R] B ⊗[R] B)
          ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x))) :
      B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.map LinearMap.id
            ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A)) :
          (a : B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
        ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x)) :
      B ⊗[R] (B ⊗[R] B))
⊢ Eq.{u_3 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ
              LinearMap.rTensor A comul ∘ₗ comul :
            (a : A) → A ⊗[R] (A ⊗[R] A))
          x) :
      B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x) :
      B ⊗[R] (B ⊗[R] B))

Tactic:
simp +instances [coalgebraStruct, e.tensorProductAssoc_def R, TensorProduct.congr,
        ← LinearMap.comp_assoc, TensorProduct.map_map, ← TensorProduct.map_comp]

Premises used: TensorProduct.map_map, LinearMap.comp_assoc, Equiv.coalgebraStruct, TensorProduct.congr, Equiv.tensorProductAssoc_def, TensorProduct.map_comp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq (α := B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.assoc R B B B : (a : B ⊗[R] B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
        ((TensorProduct.map
              ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A))
              LinearMap.id :
            (a : B ⊗[R] B) → B ⊗[R] B ⊗[R] B)
          ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x))) :
      B ⊗[R] (B ⊗[R] B))
    ((TensorProduct.map LinearMap.id
            ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A)) :
          (a : B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
        ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x)) :
      B ⊗[R] (B ⊗[R] B))

Tactic:
simpa [LinearMap.comp_assoc, -coassoc_apply] using coassoc_apply (R := R) (A := B) _

Premises used: LinearMap.comp_assoc, Coalgebra.coassoc_apply
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
h :
  ∀ (x : A),
    Eq (α := R ⊗[R] A) ((LinearMap.rTensor A counit ∘ₗ comul : (a : A) → R ⊗[R] A) x : R ⊗[R] A)
      (((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1 : (a : A) → R ⊗[R] A) x : R ⊗[R] A)
⊢ Eq (α := A →ₗ[R] R ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq (α := R ⊗[R] B)
    ((TensorProduct.map LinearMap.id (↑(linearEquiv R e) : A →ₗ[R] B) : (a : R ⊗[R] A) → R ⊗[R] B)
        ((LinearMap.rTensor A counit ∘ₗ comul : (a : A) → R ⊗[R] A) x) :
      R ⊗[R] B)
    ((TensorProduct.map LinearMap.id (↑(linearEquiv R e) : A →ₗ[R] B) : (a : R ⊗[R] A) → R ⊗[R] B)
        (((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1 : (a : A) → R ⊗[R] A) x) :
      R ⊗[R] B)

Tactic:
simpa +instances [coalgebraStruct, LinearMap.comp_assoc, TensorProduct.map_map,
        LinearMap.rTensor] using Coalgebra.rTensor_counit_comul _

Premises used: TensorProduct.map_map, LinearMap.comp_assoc, Equiv.coalgebraStruct, Coalgebra.rTensor_counit_comul, LinearMap.rTensor
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
h :
  ∀ (x : A),
    Eq (α := A ⊗[R] R) ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
      (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
⊢ Eq (α := A →ₗ[R] A ⊗[R] R) (LinearMap.lTensor A counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
h :
  Eq (α := B ⊗[R] R)
    ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
        ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x) :
      B ⊗[R] R)
    ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
        (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x) :
      B ⊗[R] R)
⊢ Eq (α := A ⊗[R] R) ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
    (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x : A ⊗[R] R)

Tactic:
apply (TensorProduct.map_bijective (g := .id) (e.linearEquiv R).bijective
        Function.bijective_id).injective

Premises used: Function.bijective_id, LinearEquiv.bijective, Equiv.linearEquiv, Function.Bijective.injective, TensorProduct.map_bijective
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq (α := B ⊗[R] R)
    ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
        ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x) :
      B ⊗[R] R)
    ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
        (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x) :
      B ⊗[R] R)

Tactic:
simpa +instances [coalgebraStruct, LinearMap.comp_assoc, TensorProduct.map_map,
        LinearMap.lTensor] using Coalgebra.lTensor_counit_comul _

Premises used: Coalgebra.lTensor_counit_comul, TensorProduct.map_map, LinearMap.comp_assoc, LinearMap.lTensor, Equiv.coalgebraStruct
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
inst_4 : IsCocomm R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this_2 : Module R A := Equiv.module R e
this : Coalgebra R A := coalgebra R e
h :
  ∀ (x : A),
    Eq (α := A ⊗[R] A)
      (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ comul : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
      ((comul : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ comul) comul

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
inst_9 : AddCommMonoid N'
inst_10 : Module R N'
inst_11 : AddCommMonoid P'
inst_12 : Module R P'
inst_13 : AddCommMonoid M₁
inst_14 : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
rw : (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ
rw₁ rw₂ : (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ

Tactic:
rw [← LinearMap.comp_assoc, TensorProduct.map_comp]

Premises used: LinearMap.comp_assoc, TensorProduct.map_comp