awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₆ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₇ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ (TensorProduct.mk R R B : (a : R) → B →ₗ[R] R ⊗[R] B) 1)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₈ hr₉ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B))
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)

Tactic:
rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]

Premises used: Prod.counit_comp_inr, LinearMap.rTensor_comp_map, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor, LinearMap.lTensor_comp_mk, Prod.comul_comp_inr
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
hl :
  Eq (α := A →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A 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)
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1)

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

Tactic:
rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← 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, Prod.comul_comp_inl, Coalgebra.lTensor_counit_comp_comul, LinearMap.lTensor_comp_map, Prod.counit_comp_inl
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
hr₈ 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)
⊢ 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)

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]

Premises used: Prod.counit_comp_inr, LinearMap.rTensor_comp_lTensor, LinearMap.rTensor_comp_flip_mk, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul, Prod.comul_comp_inr, LinearMap.lTensor_comp_map
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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))
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))
⊢ 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

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

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

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

Tactic:
lsum_single _ _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, DFinsupp.lsum_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : ι
a : A i
⊢ Eq.{u + 1} (α := R) ((counit : (a : Π₀ (i : ι), A i) → R) (single (β := A) i a) : R) ((counit : (a : A i) → R) a : R)

Tactic:
lsum_single _ _ _ _

Premises used: DFinsupp.lsum_single
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : ι
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : ι
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:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : ι
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)
⊢ 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)

Tactic:
ext j
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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
⊢ 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 : 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
this : i = j ∨ i ≠ 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:
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 : 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 : ι
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)
⊢ Eq (α := LinearMap.{u, u, w, u} (RingHom.id R) (A i) R) (counit ∘ₗ lsingle (M := A) i) counit

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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 : ι
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:
simp
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
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)
⊢ 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)

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

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

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
inst_5 : ∀ (i : ι), IsCocomm.{u, w} R (A i)
h :
  ∀ (i : ι) (x : A i),
    Eq (α := (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
      ((((↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) :
                  ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) →ₗ[R] (Π₀ (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)
      ((comul ∘ₗ lsingle (M := A) i : (a : A i) → (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) x :
        (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
⊢ Eq (α := (Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
    ((↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) :
        ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) →ₗ[R] (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) ∘ₗ
      comul)
    comul

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.Basic
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)
inst_5 : ∀ (i : ι), IsCocomm.{u, w} R (A i)
i : ι
x : A i
⊢ Eq (α := (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)
    ((((↑(TensorProduct.comm R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) :
                ((Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) →ₗ[R] (Π₀ (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)
    ((comul ∘ₗ lsingle (M := A) i : (a : A i) → (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i) x :
      (Π₀ (i : ι), A i) ⊗[R] Π₀ (i : ι), A i)

Tactic:
simp [← TensorProduct.map_comm]

Premises used: TensorProduct.map_comm
-- 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 : ι
a : A
⊢ Eq (α := (ι →₀ A) ⊗[R] (ι →₀ A))
    ((comul : (a : ι →₀ A) → (ι →₀ A) ⊗[R] (ι →₀ A)) (single i a) : (ι →₀ A) ⊗[R] (ι →₀ A))
    ((TensorProduct.map (lsingle i) (lsingle i) : (a : A ⊗[R] A) → (ι →₀ A) ⊗[R] (ι →₀ A))
        ((comul : (a : A) → A ⊗[R] A) a) :
      (ι →₀ A) ⊗[R] (ι →₀ A))

Tactic:
lsum_single _ _ _ _

Premises used: Quotient.liftOn', AddCon.liftOn, Finsupp.lsum_single
-- 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 : ι
a : A
⊢ Eq.{u + 1} (α := R) ((counit : (a : ι →₀ A) → R) (single i a) : R) ((counit : (a : A) → R) a : R)

Tactic:
lsum_single _ _ _ _

Premises used: Finsupp.lsum_single
-- 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 (α := (ι →₀ A) ⊗[R] (ι →₀ A))
      ((comul ∘ₗ lsingle i : (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A)) x : (ι →₀ A) ⊗[R] (ι →₀ A))
      ((TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul : (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A)) x :
        (ι →₀ A) ⊗[R] (ι →₀ A))
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A)) (comul ∘ₗ lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ 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 : CoalgebraStruct R A
i : ι
x : A
⊢ Eq (α := (ι →₀ A) ⊗[R] (ι →₀ A)) ((comul ∘ₗ lsingle i : (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A)) x : (ι →₀ A) ⊗[R] (ι →₀ A))
    ((TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul : (a : A) → (ι →₀ A) ⊗[R] (ι →₀ A)) x : (ι →₀ A) ⊗[R] (ι →₀ A))

Tactic:
simp