awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1)
have h : ∀ (i : n),
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₁ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
  (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₂ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
  ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₃ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₄ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map counit (LinearMap.single R A i) ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map counit (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₅ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map counit (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₆ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (rTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    (rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
    ((rTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map (counit ∘ₗ LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (map counit (LinearMap.single R A i) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit) ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
h₆ :
  Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) (lTensor R (LinearMap.single R A i) ∘ₗ rTensor (A i) counit ∘ₗ comul)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i)) ((rTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
      LinearMap.single R A i)
have h₇ : Eq (α := A i →ₗ[R] R ⊗[R] ((i : n) → A i))
  (lTensor R (LinearMap.single R A i) ∘ₗ (TensorProduct.mk R R (A i) : (a : R) → A i →ₗ[R] R ⊗[R] A i) 1)
  ((TensorProduct.mk R R ((i : n) → A i) : (a : R) → ((i : n) → A i) →ₗ[R] R ⊗[R] ((i : n) → A i)) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, rTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1)
have h : ∀ (i : n),
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₁ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
  (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₂ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
  ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← 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_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₃ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]