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 : 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)
⊢ 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
have 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)
Tactic: ext
-- 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 : CoalgebraStruct R A
i : ι
⊢ Eq (α := A →ₗ[R] (ι →₀ A) ⊗[R] (ι →₀ A)) (comul ∘ₗ lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul)
have 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))
Tactic: ext
-- 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 : CoalgebraStruct R A
i : ι
⊢ Eq (α := (ι →₀ A) →ₗ[R] A ⊗[R] A) (comul ∘ₗ lapply i) (TensorProduct.map (lapply i) (lapply i) ∘ₗ comul)
have 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)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
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
⊢ 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)
have this : i = j ∨ i ≠ j
Tactic: have := eq_or_ne i j
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : CoalgebraStruct R A
i : ι
⊢ Eq (α := A →ₗ[R] R) (counit ∘ₗ lsingle i) counit
have h : ∀ (x : A), Eq.{u + 1} (α := R) ((counit ∘ₗ lsingle i : (a : A) → R) x : R) ((counit : (a : A) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
⊢ 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)
have 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)
Tactic: ext i : 1
-- 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
⊢ Eq (α := (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) (rTensor (ι →₀ A) counit ∘ₗ comul)
    ((TensorProduct.mk R R (ι →₀ A) : (a : R) → (ι →₀ A) →ₗ[R] R ⊗[R] (ι →₀ A)) 1)
have 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)
Tactic: ext : 1
-- 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 : ι
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : 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)
⊢ 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)
have 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)
Tactic: rw [comp_assoc, comul_comp_lsingle, ← comp_assoc, rTensor_comp_map, counit_comp_lsingle,
      ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
ι : Type v
A : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R 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)
have 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)
Tactic: ext : 1
-- 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 : ι
⊢ 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) (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]
-- 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)
⊢ 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) (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)
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)
⊢ 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) ((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)
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)
⊢ 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 ∘ₗ lsingle a) ∘ₗ 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]