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
hr :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (TensorProduct.map (inr R A B) (counit ∘ₗ inr R A B) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (TensorProduct.map (inr R A B) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((rTensor R (inr R A B) ∘ₗ lTensor B counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₆ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (rTensor R (inr R A B) ∘ₗ lTensor B counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
⊢ Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
have hr₇ : Eq (α := B →ₗ[R] (A × B) ⊗[R] R)
  (rTensor R (inr R A B) ∘ₗ (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] B ⊗[R] R) 1)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
        ← 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
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] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (TensorProduct.map (inr R A B) (counit ∘ₗ inr R A B) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (TensorProduct.map (inr R A B) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((rTensor R (inr R A B) ∘ₗ lTensor B counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₆ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R) (rTensor R (inr R A B) ∘ₗ lTensor B counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
hr₇ :
  Eq (α := B →ₗ[R] (A × B) ⊗[R] R)
    (rTensor R (inr R A B) ∘ₗ (LinearMap.flip (TensorProduct.mk R B R) : (a : R) → B →ₗ[R] B ⊗[R] R) 1)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
⊢ Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
have hr₈ : Eq (α := B →ₗ[R] (A × B) ⊗[R] R)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
        ← 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
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
inst_7 : IsCocomm R A
inst_8 : IsCocomm R B
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] (A × B))
    ((↑(TensorProduct.comm R (A × B) (A × B)) : (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] (A × B)) ∘ₗ comul) comul
have hl : ∀ (x : A),
  Eq (α := (A × B) ⊗[R] (A × B))
    ((((↑(TensorProduct.comm R (A × B) (A × B)) : (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] (A × B)) ∘ₗ comul) ∘ₗ
            inl R A B :
          (a : A) → (A × B) ⊗[R] (A × B))
        x :
      (A × B) ⊗[R] (A × B))
    ((comul ∘ₗ inl R A B : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
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
inst_7 : IsCocomm R A
inst_8 : IsCocomm R B
hl :
  ∀ (x : A),
    Eq (α := (A × B) ⊗[R] (A × B))
      ((((↑(TensorProduct.comm R (A × B) (A × B)) : (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] (A × B)) ∘ₗ comul) ∘ₗ
              inl R A B :
            (a : A) → (A × B) ⊗[R] (A × B))
          x :
        (A × B) ⊗[R] (A × B))
      ((comul ∘ₗ inl R A B : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] (A × B))
    ((↑(TensorProduct.comm R (A × B) (A × B)) : (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] (A × B)) ∘ₗ comul) comul
have hr : ∀ (x : B),
  Eq (α := (A × B) ⊗[R] (A × B))
    ((((↑(TensorProduct.comm R (A × B) (A × B)) : (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] (A × B)) ∘ₗ comul) ∘ₗ
            inr R A B :
          (a : B) → (A × B) ⊗[R] (A × B))
        x :
      (A × B) ⊗[R] (A × B))
    ((comul ∘ₗ inr R A B : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
Tactic: ext
-- 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 : ι) → CoalgebraStruct.{u, w} R (A i)
i : ι
⊢ Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) (comul ∘ₗ lsingle (M := A) i)
    (TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul)
have h : ∀ (x : A i),
  Eq (α := (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
    ((comul ∘ₗ lsingle (M := A) i : (a : A i) → (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) x :
      (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
    ((TensorProduct.map (lsingle (M := A) i) (lsingle (M := A) i) ∘ₗ comul :
          (a : A i) → (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
        x :
      (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
Tactic: ext
-- 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 : ι) → CoalgebraStruct.{u, w} R (A i)
i : ι
⊢ Eq (α := (Π₀ (i : ι), A i) →ₗ[R] A i ⊗[R] A i) (comul ∘ₗ lapply (M := A) i)
    (TensorProduct.map (lapply (M := A) i) (lapply (M := A) i) ∘ₗ comul)
have h : ∀ (j : ι) (x : A j),
  Eq (α := A i ⊗[R] A i)
    (((comul ∘ₗ lapply (M := A) i) ∘ₗ lsingle (M := A) j : (a : A j) → A i ⊗[R] A i) x : A i ⊗[R] A i)
    (((TensorProduct.map (lapply (M := A) i) (lapply (M := A) i) ∘ₗ comul) ∘ₗ lsingle (M := A) j :
          (a : A j) → A i ⊗[R] A i)
        x :
      A i ⊗[R] A i)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
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 : ι) → CoalgebraStruct.{u, w} R (A i)
i j : ι
x : A j
⊢ Eq (α := A i ⊗[R] A i)
    (((comul ∘ₗ lapply (M := A) i) ∘ₗ lsingle (M := A) j : (a : A j) → A i ⊗[R] A i) x : A i ⊗[R] A i)
    (((TensorProduct.map (lapply (M := A) i) (lapply (M := A) i) ∘ₗ comul) ∘ₗ lsingle (M := A) j :
          (a : A j) → A i ⊗[R] A i)
        x :
      A i ⊗[R] A i)
have this : i = j ∨ i ≠ j
Tactic: have := eq_or_ne i j
-- 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 : ι) → CoalgebraStruct.{u, w} R (A i)
i : ι
⊢ Eq (α := LinearMap.{u, u, w, u} (RingHom.id R) (A i) R) (counit ∘ₗ lsingle (M := A) i) counit
have h : ∀ (x : A i), Eq.{u + 1} (α := R) ((counit ∘ₗ lsingle (M := A) i : (a : A i) → R) x : R) ((counit : (a : A i) → R) x : R)
Tactic: ext
-- 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] ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i))
    ((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) :
        (((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) →ₗ[R]
          (Π₀ (i : ι), A i) ⊗[R] ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul)
    (lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul)
have h : ∀ (i : ι),
  Eq (α := A i →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i))
    (((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) :
          (((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) →ₗ[R]
            (Π₀ (i : ι), A i) ⊗[R] ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)) ∘ₗ
        rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ
      lsingle (M := A) i)
    ((lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul) ∘ₗ lsingle (M := A) i)
Tactic: ext i : 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)
⊢ Eq (α := (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) (rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R (Π₀ (i : ι), A i) : (a : R) → (Π₀ (i : ι), A i) →ₗ[R] R ⊗[R] Π₀ (i : ι), A i) 1)
have h : ∀ (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)
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] 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) (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)
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)
⊢ 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)
  (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)
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)
⊢ 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)
  ((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)
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)
⊢ 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.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)
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)
⊢ 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.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)
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)
⊢ 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]