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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : ι
h :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) (counit ∘ₗ lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
have h₄ : Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : ι
h :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) (counit ∘ₗ lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₄ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
have h₅ : Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((rTensor R (lsingle a) ∘ₗ lTensor A counit) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : ι
h :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) (counit ∘ₗ lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₄ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₅ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((rTensor R (lsingle a) ∘ₗ lTensor A counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
have h₆ : Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (rTensor R (lsingle a) ∘ₗ lTensor A counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : ι
h :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) (counit ∘ₗ lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₄ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₅ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((rTensor R (lsingle a) ∘ₗ lTensor A counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₆ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (rTensor R (lsingle a) ∘ₗ lTensor A counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
have h₇ : Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R)
  (rTensor R (lsingle a) ∘ₗ (LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
a : ι
h :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) (counit ∘ₗ lsingle a) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₄ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (TensorProduct.map (lsingle a) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₅ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((rTensor R (lsingle a) ∘ₗ lTensor A counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₆ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) (rTensor R (lsingle a) ∘ₗ lTensor A counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
h₇ :
  Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R)
    (rTensor R (lsingle a) ∘ₗ (LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R) ((lTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
have h₈ : Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] R)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
  ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1 ∘ₗ lsingle a)
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 : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
inst_4 : IsCocomm R A
⊢ Eq (α := (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A))
    ((↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) : (ι →₀ A) ⊗[R] (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A)) ∘ₗ comul) comul
have h : ∀ (a : ι) (x : A),
  Eq (α := (ι →₀ A) ⊗[R] (ι →₀ A))
    ((((↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) : (ι →₀ A) ⊗[R] (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A)) ∘ₗ comul) ∘ₗ
            lsingle a :
          (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A))
        x :
      (ι →₀ A) ⊗[R] (ι →₀ A))
    ((comul ∘ₗ lsingle a : (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A)) x : (ι →₀ A) ⊗[R] (ι →₀ A))
Tactic: ext
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
i : n
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i)) (comul ∘ₗ LinearMap.single R A i)
    (map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
have h : ∀ (x : A i),
  Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ LinearMap.single R A i : (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul : (a : A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
Tactic: ext
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
i : n
⊢ Eq (α := ((i : n) → A i) →ₗ[R] A i ⊗[R] A i) (comul ∘ₗ proj (φ := A) i)
    (map (proj (φ := A) i) (proj (φ := A) i) ∘ₗ comul)
have h : ∀ (j : n) (x : A j),
  Eq (α := A i ⊗[R] A i)
    (((comul ∘ₗ proj (φ := A) i) ∘ₗ LinearMap.single R A j : (a : A j) → A i ⊗[R] A i) x : A i ⊗[R] A i)
    (((map (proj (φ := A) i) (proj (φ := A) i) ∘ₗ comul) ∘ₗ LinearMap.single R 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_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) → CoalgebraStruct.{u_1, u_3} R (A i)
i j : n
x : A j
⊢ Eq (α := A i ⊗[R] A i)
    (((comul ∘ₗ proj (φ := A) i) ∘ₗ LinearMap.single R A j : (a : A j) → A i ⊗[R] A i) x : A i ⊗[R] A i)
    (((map (proj (φ := A) i) (proj (φ := A) i) ∘ₗ comul) ∘ₗ LinearMap.single R 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_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) → CoalgebraStruct.{u_1, u_3} R (A i)
i : n
⊢ Eq (α := LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (A i) R) (counit ∘ₗ LinearMap.single R A i) counit
have h : ∀ (x : A i),
  Eq.{u_1 + 1} (α := R) ((counit ∘ₗ LinearMap.single R 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_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) → CoalgebraStruct.{u_1, u_3} R (A i)
⊢ Eq (α := (Π₀ (i : n), A i) →ₗ[R] R) (counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A)) counit
have apply : ∀ (x : Π₀ (i : n), A i),
  Eq.{u_1 + 1} (α := R) ((counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → R) x : R)
    ((counit : (a : Π₀ (i : n), A i) → R) x : R)
Tactic: apply LinearMap.ext fun x ↦ ?_
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
⊢ Eq.{u_1 + 1} (α := R) ((counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → R) x : R)
    ((counit : (a : Π₀ (i : n), A i) → R) x : R)
have have : ∀ (this : (i : n) → (x : A i) → Decidable (x ≠ 0)),
  Eq.{u_1 + 1} (α := R) ((counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → R) x : R)
    ((counit : (a : Π₀ (i : n), A i) → R) x : R)
Tactic: have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
this : (i : n) → (x : A i) → Decidable (x ≠ 0)
⊢ Eq.{u_1 + 1} (α := R) ((counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → R) x : R)
    ((counit : (a : Π₀ (i : n), A i) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R)
  ((counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → R)
      (x.sum (β := A) (DFinsupp.single (β := A))) :
    R)
  ((counit : (a : Π₀ (i : n), A i) → R) (x.sum (β := A) (DFinsupp.single (β := A))) : R)
Tactic: rw [← DFinsupp.sum_single (f := x)]
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
⊢ Eq (α := (Π₀ (i : n), A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i)) (comul ∘ₗ coeFnLinearMap R (β := A))
    (map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul)
have apply : ∀ (x : Π₀ (i : n), A i),
  Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
          (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
Tactic: apply LinearMap.ext fun x ↦ ?_
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
⊢ Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
          (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
have have : ∀ (this : (i : n) → (x : A i) → Decidable (x ≠ 0)),
  Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
          (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
Tactic: have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _
-- 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) → CoalgebraStruct.{u_1, u_3} R (A i)
x : Π₀ (i : n), A i
this : (i : n) → (x : A i) → Decidable (x ≠ 0)
⊢ Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i)) x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
          (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        x :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))
have rw : Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
  ((comul ∘ₗ coeFnLinearMap R (β := A) : (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
      (x.sum (β := A) (DFinsupp.single (β := A))) :
    ((i : n) → A i) ⊗[R] ((i : n) → A i))
  ((map (coeFnLinearMap R (β := A)) (coeFnLinearMap R (β := A)) ∘ₗ comul :
        (a : Π₀ (i : n), A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
      (x.sum (β := A) (DFinsupp.single (β := A))) :
    ((i : n) → A i) ⊗[R] ((i : n) → A i))
Tactic: rw [← DFinsupp.sum_single (f := x)]
-- 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
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
⊢ Eq (α := (n →₀ M) →ₗ[R] R) (counit ∘ₗ Finsupp.lcoeFun) counit
have apply : ∀ (x : n →₀ M),
  Eq.{u_1 + 1} (α := R) ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) x : R) ((counit : (a : n →₀ M) → R) x : R)
Tactic: apply LinearMap.ext fun x ↦ ?_
-- 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
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq.{u_1 + 1} (α := R) ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) x : R) ((counit : (a : n →₀ M) → R) x : R)
have rw : Eq.{u_1 + 1} (α := R)
  ((counit ∘ₗ Finsupp.lcoeFun : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)
  ((counit : (a : n →₀ M) → R) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)) : R)
Tactic: rw [← Finsupp.univ_sum_single x]
-- 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
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
⊢ Eq (α := (n →₀ M) →ₗ[R] (n → M) ⊗[R] (n → M)) (comul ∘ₗ lcoeFun) (map lcoeFun lcoeFun ∘ₗ comul)
have apply : ∀ (x : n →₀ M),
  Eq (α := (n → M) ⊗[R] (n → M)) ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
    ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
Tactic: apply LinearMap.ext fun x ↦ ?_
-- 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
M : Type u_4
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : CoalgebraStruct R M
x : n →₀ M
⊢ Eq (α := (n → M) ⊗[R] (n → M)) ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
    ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) x : (n → M) ⊗[R] (n → M))
have rw : Eq (α := (n → M) ⊗[R] (n → M))
  ((comul ∘ₗ lcoeFun : (a : n →₀ M) → (n → M) ⊗[R] (n → M)) (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))
  ((map lcoeFun lcoeFun ∘ₗ comul : (a : n →₀ M) → (n → M) ⊗[R] (n → M))
    (∑ a : n, Finsupp.single a ((x : (a : n) → M) a)))
Tactic: rw [← Finsupp.univ_sum_single x]
-- 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] (((i : n) → A i) ⊗[R] ((i : n) → A i)))
    ((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) :
        ((i : n) → A i) ⊗[R] ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R]
          ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i))) ∘ₗ
      rTensor ((i : n) → A i) comul ∘ₗ comul)
    (lTensor ((i : n) → A i) comul ∘ₗ comul)
have h : ∀ (i : n),
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i)))
    (((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) :
          ((i : n) → A i) ⊗[R] ((i : n) → A i) ⊗[R] ((i : n) → A i) →ₗ[R]
            ((i : n) → A i) ⊗[R] (((i : n) → A i) ⊗[R] ((i : n) → A i))) ∘ₗ
        rTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ
      LinearMap.single R A i)
    ((lTensor ((i : n) → A i) comul ∘ₗ comul) ∘ₗ LinearMap.single R A i)
Tactic: ext : 1