awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hl₇ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 (TensorProduct.map 0 0 ∘ₗ comul)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hl₈ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 (0 ∘ₗ comul)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hl₉ : Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) 0 0
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hr₇ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hr₈ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul (LinearMap.id ∘ₗ comul)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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)
⊢ 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)
have hr₉ : Eq.{w + 1} (α := B →ₗ[R] B ⊗[R] B) comul comul
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := B →ₗ[R] R) (counit ∘ₗ inr R A B) counit
have h : ∀ (x : B), Eq.{u + 1} (α := R) ((counit ∘ₗ inr R A B : (a : B) → R) x : R) ((counit : (a : B) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ inl R A B) counit
have h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ inl R A B : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
        (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (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)) ∘ₗ
        coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul))
    (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)) ∘ₗ
      coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul))
have hl : ∀ (x : A),
  Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
                (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (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)) ∘ₗ
                coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inl R A B :
          (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × 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)) ∘ₗ
              coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inl R A B :
          (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: ext x : 2