awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (TensorProduct.map (counit ∘ₗ lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (TensorProduct.map counit (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
have h₆ : Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
  ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (TensorProduct.map (counit ∘ₗ lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (TensorProduct.map counit (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₆ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
have h₇ : Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
  (lTensor R (lsingle (M := A) i) ∘ₗ (TensorProduct.mk R R (A i) : (a : R) → A i →ₗ[R] R ⊗[R] A i) 1)
  ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (TensorProduct.map (counit ∘ₗ lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (TensorProduct.map counit (lsingle (M := A) i) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₆ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (lTensor R (lsingle (M := A) i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
h₇ :
  Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
    (lTensor R (lsingle (M := A) i) ∘ₗ (TensorProduct.mk R R (A i) : (a : R) → A i →ₗ[R] R ⊗[R] A i) 1)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) ((rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
      lsingle (M := A) i)
have h₈ : Eq (α := A i →ₗ[R] R ⊗[R] Π₀ (i : ι), A i)
  ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
    lsingle (M := A) i)
  ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
⊢ Eq (α := (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1)
have h : ∀ (i : ι),
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₁ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
  (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₂ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
  ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₃ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
  (TensorProduct.map (lsingle (M := A) i) (counit ∘ₗ lsingle (M := A) i) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (TensorProduct.map (lsingle (M := A) i) (counit ∘ₗ lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₄ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (TensorProduct.map (lsingle (M := A) i) counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (TensorProduct.map (lsingle (M := A) i) (counit ∘ₗ lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (TensorProduct.map (lsingle (M := A) i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₅ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((rTensor R (lsingle (M := A) i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : ι → Type w
inst : DecidableEq ι
inst_1 : CommSemiring R
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : (i : ι) → Module.{u, w} R (A i)
inst_4 : (i : ι) → Coalgebra.{u, w} R (A i)
i : ι
h :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₁ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₂ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₃ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
    (TensorProduct.map (lsingle (M := A) i) (counit ∘ₗ lsingle (M := A) i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₄ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (TensorProduct.map (lsingle (M := A) i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
h₅ :
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((rTensor R (lsingle (M := A) i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) ((lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul) ∘ₗ lsingle (M := A) i)
    ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
          (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
        1 ∘ₗ
      lsingle (M := A) i)
have h₆ : Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R) (rTensor R (lsingle (M := A) i) ∘ₗ lTensor (A i) counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (Π₀ (i : ι), A i) R) :
        (a : R) → (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] R)
      1 ∘ₗ
    lsingle (M := A) i)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, lTensor_comp_map, counit_comp_lsingle,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]