awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
r : A × B
⊢ (counit : (a : A × B) → R) r =
    HAdd.hAdd (α := R) (β := R) ((counit : (a : A) → R) r.1 : R) ((counit : (a : B) → R) r.2 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h :
  ∀ (x : A),
    Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inl R A B : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
      ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
⊢ Eq (α := A →ₗ[R] (A × B) ⊗[R] (A × B)) (comul ∘ₗ inl R A B) (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : A
⊢ Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inl R A B : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
    ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h :
  ∀ (x : B),
    Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inr R A B : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
      ((TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
⊢ Eq (α := B →ₗ[R] (A × B) ⊗[R] (A × B)) (comul ∘ₗ inr R A B) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : B
⊢ Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inr R A B : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
    ((TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hr :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
⊢ Eq (α := A × B →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B)
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
hl₆ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul)
hl₇ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
hl₈ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (LinearMap.id ∘ₗ comul)
hl₉ hl₁₀ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul comul
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)

Tactic:
rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]

Premises used: LinearMap.comp_assoc, TensorProduct.map_comp, LinearMap.fst_comp_inl, LinearMap.comp_id, Prod.comul_comp_inl, LinearMap.id_comp, TensorProduct.map_id
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hr :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₁ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ 0)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₂ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₃ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inr R A B)
hr₄ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
hr₅ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
      comul)
hr₆ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    (TensorProduct.map (LinearMap.fst R A B ∘ₗ inr R A B) (LinearMap.fst R A B ∘ₗ inr R A B) ∘ₗ comul)
hr₇ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0 (TensorProduct.map 0 0 ∘ₗ comul)
hr₈ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0 (0 ∘ₗ comul)
hr₉ hr₁₀ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0 0
⊢ Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)

Tactic:
rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]

Premises used: LinearMap.fst_comp_inr, LinearMap.comp_assoc, LinearMap.comp_zero, TensorProduct.map_comp, TensorProduct.map_zero_left, Prod.comul_comp_inr, LinearMap.zero_comp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) ((comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B)
hr :
  Eq (α := B →ₗ[R] B ⊗[R] B) ((comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B)
⊢ Eq (α := A × B →ₗ[R] B ⊗[R] B) (comul ∘ₗ LinearMap.snd R A B)
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) (comul ∘ₗ LinearMap.snd R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) (comul ∘ₗ 0)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
hl₆ :
  Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0
    (TensorProduct.map (LinearMap.snd R A B ∘ₗ inl R A B) (LinearMap.snd R A B ∘ₗ inl R A B) ∘ₗ comul)
hl₇ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 (TensorProduct.map 0 0 ∘ₗ comul)
hl₈ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 (0 ∘ₗ comul)
hl₉ hl₁₀ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 0
⊢ Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) ((comul ∘ₗ LinearMap.snd R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inl R A B)

Tactic:
rw [comp_assoc, snd_comp_inl, comp_zero, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, snd_comp_inl, TensorProduct.map_zero_left, zero_comp]

Premises used: LinearMap.comp_assoc, LinearMap.snd_comp_inl, LinearMap.comp_zero, TensorProduct.map_comp, TensorProduct.map_zero_left, Prod.comul_comp_inl, LinearMap.zero_comp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hr :
  Eq (α := B →ₗ[R] B ⊗[R] B) (comul ∘ₗ LinearMap.snd R A B ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] B ⊗[R] B) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] B ⊗[R] B) comul
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] B ⊗[R] B) comul (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] B ⊗[R] B) comul
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ
      TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
hr₅ :
  Eq (α := B →ₗ[R] B ⊗[R] B) comul
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ
      comul)
hr₆ :
  Eq (α := B →ₗ[R] B ⊗[R] B) comul
    (TensorProduct.map (LinearMap.snd R A B ∘ₗ inr R A B) (LinearMap.snd R A B ∘ₗ inr R A B) ∘ₗ comul)
hr₇ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
hr₈ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul (LinearMap.id ∘ₗ comul)
hr₉ hr₁₀ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul comul
⊢ Eq (α := B →ₗ[R] B ⊗[R] B) ((comul ∘ₗ LinearMap.snd R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B)

Tactic:
rw [comp_assoc, snd_comp_inr, comp_id, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, snd_comp_inr, TensorProduct.map_id, id_comp]

Premises used: LinearMap.comp_assoc, TensorProduct.map_comp, LinearMap.snd_comp_inr, LinearMap.comp_id, Prod.comul_comp_inr, LinearMap.id_comp, TensorProduct.map_id
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h : ∀ (x : B), Eq.{u + 1} (α := R) ((counit ∘ₗ inr R A B : (a : B) → R) x : R) ((counit : (a : B) → R) x : R)
⊢ Eq (α := B →ₗ[R] R) (counit ∘ₗ inr R A B) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : B
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ inr R A B : (a : B) → R) x : R) ((counit : (a : B) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ inl R A B : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ inl R A B) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : A
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ inl R A B : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : A
hl :
  Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
            ((comul : (a : A) → A ⊗[R] A) x))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
          ((comul : (a : A) → A ⊗[R] A) x)) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
                ((comul : (a : A) → A ⊗[R] A) x) :
              (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
                ((comul : (a : B) → B ⊗[R] B) 0) :
              (A × B) ⊗[R] (A × B)))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) x) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) 0) :
            (A × B) ⊗[R] (A × B))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))

Tactic:
simp only [map_zero, add_zero]

Premises used: map_zero, add_zero
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
x : B
hr :
  Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
            ((comul : (a : B) → B ⊗[R] B) x))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
          ((comul : (a : B) → B ⊗[R] B) x)) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
                ((comul : (a : A) → A ⊗[R] A) 0) :
              (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
                ((comul : (a : B) → B ⊗[R] B) x) :
              (A × B) ⊗[R] (A × B)))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) 0) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) x) :
            (A × B) ⊗[R] (A × B))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))

Tactic:
simp only [map_zero, zero_add]

Premises used: map_zero, zero_add
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hr :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ Eq (α := A × B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₅ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inl R A B) ∘ₗ rTensor A counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₆ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inl R A B) ∘ₗ rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₇ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inl R A B) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₈ hl₉ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B))
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)

Tactic:
rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Premises used: LinearMap.rTensor_comp_map, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, LinearMap.lTensor_comp_mk, Prod.comul_comp_inl, Prod.counit_comp_inl