awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i : ι
h :
  ∀ (j : ι) (x : A),
    Eq (α := A ⊗[R] A) (((comul ∘ₗ lapply i) ∘ₗ lsingle j : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
      (((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
⊢ Eq (α := (ι →₀ A) →ₗ[R] A ⊗[R] A) (comul ∘ₗ lapply i) (TensorProduct.map (lapply i) (lapply i) ∘ₗ comul)

Tactic:
ext j
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i j : ι
x : A
⊢ i = j ∨ i ≠ j

Tactic:
have := eq_or_ne i j
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i j : ι
x : A
this : i = j ∨ i ≠ j
⊢ Eq (α := A ⊗[R] A) (((comul ∘ₗ lapply i) ∘ₗ lsingle j : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
    (((TensorProduct.map (lapply i) (lapply i) ∘ₗ comul) ∘ₗ lsingle j : (a : A) → A ⊗[R] A) x : A ⊗[R] A)

Tactic:
aesop (add simp [TensorProduct.map_map, proj_comp_single, diag])

Premises used: TensorProduct.map_map, LinearMap.proj_comp_single, LinearMap.diag
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i : ι
h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ lsingle i : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ lsingle i) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i : ι
x : A
⊢ Eq.{u + 1} (α := R) ((counit ∘ₗ lsingle i : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h :
  ∀ (i : ι),
    Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] ((ι →₀ A) ⊗[R] (ι →₀ A)))
      (((↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) :
            (ι →₀ A) ⊗[R] (ι →₀ A) ⊗[R] (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] ((ι →₀ A) ⊗[R] (ι →₀ A))) ∘ₗ
          rTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ
        lsingle i)
      ((lTensor (ι →₀ A) comul ∘ₗ comul) ∘ₗ lsingle i)
⊢ Eq (α := (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] ((ι →₀ A) ⊗[R] (ι →₀ A)))
    ((↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) :
        (ι →₀ A) ⊗[R] (ι →₀ A) ⊗[R] (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] ((ι →₀ A) ⊗[R] (ι →₀ A))) ∘ₗ
      rTensor (ι →₀ A) comul ∘ₗ comul)
    (lTensor (ι →₀ A) comul ∘ₗ comul)

Tactic:
ext i : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h :
  ∀ (a : ι),
    Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) ((rTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
      ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
⊢ Eq (α := (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) (rTensor (ι →₀ A) counit ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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] R ⊗[R] (ι →₀ A)) (rTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) (rTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a) ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) ((rTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a) (lsingle a)) ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₃ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) (TensorProduct.map (counit ∘ₗ lsingle a) (lsingle a) ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₄ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) (TensorProduct.map counit (lsingle a) ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₅ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) ((lTensor R (lsingle a) ∘ₗ rTensor A counit) ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₆ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) (lTensor R (lsingle a) ∘ₗ rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₇ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) (lTensor R (lsingle a) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
h₈ h₉ :
  Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A))
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (ι →₀ A)) ((rTensor (ι →₀ A) counit ∘ₗ comul) ∘ₗ lsingle a)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1 ∘ₗ lsingle a)

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]

Premises used: LinearMap.rTensor_comp_map, LinearMap.comp_assoc, Finsupp.counit_comp_lsingle, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, LinearMap.lTensor_comp_mk, Finsupp.comul_comp_lsingle
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
h :
  ∀ (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)
⊢ Eq (α := (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) (lTensor (ι →₀ A) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (ι →₀ A) R) : (a : R) → (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] R) 1)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
h₈ 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)
⊢ 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)

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]

Premises used: LinearMap.rTensor_comp_lTensor, LinearMap.rTensor_comp_flip_mk, LinearMap.comp_assoc, Finsupp.counit_comp_lsingle, Coalgebra.lTensor_counit_comp_comul, Finsupp.comul_comp_lsingle, LinearMap.lTensor_comp_map
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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))
⊢ Eq (α := (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A))
    ((↑(TensorProduct.comm R (ι →₀ A) (ι →₀ A)) : (ι →₀ A) ⊗[R] (ι →₀ A) →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A)) ∘ₗ comul) comul

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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:
simp [← TensorProduct.map_comm]

Premises used: TensorProduct.map_comm
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
a : A i
⊢ Eq (α := ((j : n) → A j) ⊗[R] ((j : n) → A j))
    ((comul : (a : (j : n) → A j) → ((j : n) → A j) ⊗[R] ((j : n) → A j)) (single (M := A) i a) :
      ((j : n) → A j) ⊗[R] ((j : n) → A j))
    ((map (LinearMap.single R A i) (LinearMap.single R A i) : (a : A i ⊗[R] A i) → ((i : n) → A i) ⊗[R] ((i : n) → A i))
        ((comul : (a : A i) → A i ⊗[R] A i) a) :
      ((i : n) → A i) ⊗[R] ((i : n) → A i))

Tactic:
lsum_piSingle _ _ _ _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.lsum_piSingle
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
a : A i
⊢ Eq.{u_1 + 1} (α := R) ((counit : (a : (j : n) → A j) → R) (single (M := A) i a) : R) ((counit : (a : A i) → R) a : R)

Tactic:
lsum_piSingle _ _ _ _ _ _

Premises used: LinearMap.lsum_piSingle
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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))
⊢ 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)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] A i ⊗[R] A i) (comul ∘ₗ proj (φ := A) i)
    (map (proj (φ := A) i) (proj (φ := A) i) ∘ₗ comul)

Tactic:
ext j
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
⊢ i = j ∨ i ≠ j

Tactic:
have := eq_or_ne i j
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
this : i = j ∨ i ≠ 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:
aesop (add simp [map_map, proj_comp_single, diag])

Premises used: TensorProduct.map_map, LinearMap.proj_comp_single, LinearMap.diag
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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)
⊢ Eq (α := LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (A i) R) (counit ∘ₗ LinearMap.single R A i) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
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)
⊢ Eq (α := (Π₀ (i : n), A i) →ₗ[R] R) (counit ∘ₗ DFinsupp.coeFnLinearMap R (β := A)) counit

Tactic:
apply LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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)
⊢ 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 _
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
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)
⊢ 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:
rw [← DFinsupp.sum_single (f := x)]

Premises used: DFinsupp.sum_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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.sum (β := A) (DFinsupp.single (β := A))) :
      R)
    ((counit : (a : Π₀ (i : n), A i) → R) (x.sum (β := A) (DFinsupp.single (β := A))) : R)

Tactic:
simp [DFinsupp.single_eq_pi_single]

Premises used: DFinsupp.single_eq_pi_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : (a : (a : n) → A a) → R) (⇑x : (a : n) → A a) : R)
    ((counit : (a : Π₀ (i : n), A i) → R) x : R)

Tactic:
congr($counit_comp_dFinsuppCoeFnLinearMap x)

Premises used: congrArg, Pi.counit_comp_dFinsuppCoeFnLinearMap, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
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))
⊢ 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)

Tactic:
apply LinearMap.ext fun x ↦ ?_

Premises used: LinearMap.ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
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))
⊢ 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 _
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
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))
⊢ 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:
rw [← DFinsupp.sum_single (f := x)]

Premises used: DFinsupp.sum_single