awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₄ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₅ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₆ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
i : n
h :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (lTensor ((i : n) → A i) counit ∘ₗ comul ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₁ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₂ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
    ((lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i) (LinearMap.single R A i)) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₃ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) (counit ∘ₗ LinearMap.single R A i) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₄ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (map (LinearMap.single R A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₅ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
h₆ :
  Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) (rTensor R (LinearMap.single R A i) ∘ₗ lTensor (A i) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
⊢ Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R) ((lTensor ((i : n) → A i) counit ∘ₗ comul) ∘ₗ LinearMap.single R A i)
    ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R)
        1 ∘ₗ
      LinearMap.single R A i)
have h₇ : Eq (α := A i →ₗ[R] ((i : n) → A i) ⊗[R] R)
  (rTensor R (LinearMap.single R A i) ∘ₗ
    (LinearMap.flip (TensorProduct.mk R (A i) R) : (a : R) → A i →ₗ[R] A i ⊗[R] R) 1)
  ((LinearMap.flip (TensorProduct.mk R ((i : n) → A i) R) : (a : R) → ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] R) 1 ∘ₗ
    LinearMap.single R A i)
Tactic: rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
A : n → Type u_3
inst_3 : (i : n) → AddCommMonoid (A i)
inst_4 : (i : n) → Module.{u_1, u_3} R (A i)
inst_5 : (i : n) → Coalgebra.{u_1, u_3} R (A i)
inst_6 : ∀ (i : n), IsCocomm.{u_1, u_3} R (A i)
⊢ Eq (α := ((i : n) → A i) →ₗ[R] ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((↑(TensorProduct.comm R ((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)) ∘ₗ
      comul)
    comul
have h : ∀ (i : n) (x : A i),
  Eq (α := ((i : n) → A i) ⊗[R] ((i : n) → A i))
    ((((↑(TensorProduct.comm R ((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)) ∘ₗ
              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))
    ((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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ 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)) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul)
    (LinearMap.lTensor A comul ∘ₗ comul)
have h : ∀ (x : A),
  Eq (α := A ⊗[R] (A ⊗[R] A))
    (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul :
          (a : A) → A ⊗[R] (A ⊗[R] A))
        x :
      A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x : A ⊗[R] (A ⊗[R] A))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq (α := A ⊗[R] (A ⊗[R] A))
    (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ LinearMap.rTensor A comul ∘ₗ comul :
          (a : A) → A ⊗[R] (A ⊗[R] A))
        x :
      A ⊗[R] (A ⊗[R] A))
    ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x : A ⊗[R] (A ⊗[R] A))
have h : Eq.{u_3 + 1} (α := B ⊗[R] (B ⊗[R] B))
  (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
            (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ
            LinearMap.rTensor A comul ∘ₗ comul :
          (a : A) → A ⊗[R] (A ⊗[R] A))
        x) :
    B ⊗[R] (B ⊗[R] B))
  (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
            (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
        (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
      ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x) :
    B ⊗[R] (B ⊗[R] B))
Tactic: apply (TensorProduct.map_bijective (e.linearEquiv R).bijective <|
        TensorProduct.map_bijective (e.linearEquiv R).bijective
        (e.linearEquiv R).bijective).injective
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq.{u_3 + 1} (α := B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        (((↑(TensorProduct.assoc R A A A) : A ⊗[R] A ⊗[R] A →ₗ[R] A ⊗[R] (A ⊗[R] A)) ∘ₗ
              LinearMap.rTensor A comul ∘ₗ comul :
            (a : A) → A ⊗[R] (A ⊗[R] A))
          x) :
      B ⊗[R] (B ⊗[R] B))
    (((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B)
              (TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) (↑(linearEquiv R e) : A →ₗ[R] B)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (A ⊗[R] (A ⊗[R] A)) (B ⊗[R] (B ⊗[R] B))) :
          (a : A ⊗[R] (A ⊗[R] A)) → B ⊗[R] (B ⊗[R] B))
        ((LinearMap.lTensor A comul ∘ₗ comul : (a : A) → A ⊗[R] (A ⊗[R] A)) x) :
      B ⊗[R] (B ⊗[R] B))
have h : Eq (α := B ⊗[R] (B ⊗[R] B))
  ((TensorProduct.assoc R B B B : (a : B ⊗[R] B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
      ((TensorProduct.map
            ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A))
            LinearMap.id :
          (a : B ⊗[R] B) → B ⊗[R] B ⊗[R] B)
        ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x))) :
    B ⊗[R] (B ⊗[R] B))
  ((TensorProduct.map LinearMap.id
          ((comul ∘ₗ (↑(linearEquiv R e) : A →ₗ[R] B)) ∘ₗ (↑(LinearEquiv.symm (linearEquiv R e)) : B →ₗ[R] A)) :
        (a : B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
      ((comul : (a : B) → B ⊗[R] B) ((linearEquiv R e : (a : A) → B) x)) :
    B ⊗[R] (B ⊗[R] B))
Tactic: simp +instances [coalgebraStruct, e.tensorProductAssoc_def R, TensorProduct.congr,
        ← LinearMap.comp_assoc, TensorProduct.map_map, ← TensorProduct.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ Eq (α := A →ₗ[R] R ⊗[R] A) (LinearMap.rTensor A counit ∘ₗ comul)
    ((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
have h : ∀ (x : A),
  Eq (α := R ⊗[R] A) ((LinearMap.rTensor A counit ∘ₗ comul : (a : A) → R ⊗[R] A) x : R ⊗[R] A)
    (((TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1 : (a : A) → R ⊗[R] A) x : R ⊗[R] A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
⊢ Eq (α := A →ₗ[R] A ⊗[R] R) (LinearMap.lTensor A counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1)
have h : ∀ (x : A),
  Eq (α := A ⊗[R] R) ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
    (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this : Module R A := Equiv.module R e
x : A
⊢ Eq (α := A ⊗[R] R) ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
    (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x : A ⊗[R] R)
have h : Eq (α := B ⊗[R] R)
  ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
      ((LinearMap.lTensor A counit ∘ₗ comul : (a : A) → A ⊗[R] R) x) :
    B ⊗[R] R)
  ((TensorProduct.map (↑(linearEquiv R e) : A →ₗ[R] B) LinearMap.id : (a : A ⊗[R] R) → B ⊗[R] R)
      (((LinearMap.flip (TensorProduct.mk R A R) : (a : R) → A →ₗ[R] A ⊗[R] R) 1 : (a : A) → A ⊗[R] R) x) :
    B ⊗[R] R)
Tactic: apply (TensorProduct.map_bijective (g := .id) (e.linearEquiv R).bijective
        Function.bijective_id).injective
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid B
inst_2 : Module R B
inst_3 : Coalgebra R B
inst_4 : IsCocomm R B
e : A ≃ B
this_1 : AddCommMonoid A := e.addCommMonoid
this_2 : Module R A := Equiv.module R e
this : Coalgebra R A := coalgebra R e
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ comul) comul
have h : ∀ (x : A),
  Eq (α := A ⊗[R] A)
    (((↑(TensorProduct.comm R A A) : A ⊗[R] A →ₗ[R] A ⊗[R] A) ∘ₗ comul : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
    ((comul : (a : A) → A ⊗[R] A) x : A ⊗[R] A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
inst_9 : AddCommMonoid N'
inst_10 : Module R N'
inst_11 : AddCommMonoid P'
inst_12 : Module R P'
inst_13 : AddCommMonoid M₁
inst_14 : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ
have rw : (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ
Tactic: rw [← LinearMap.comp_assoc, TensorProduct.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
M₁ : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
inst_9 : AddCommMonoid N'
inst_10 : Module R N'
inst_11 : AddCommMonoid P'
inst_12 : Module R P'
inst_13 : AddCommMonoid M₁
inst_14 : Module R M₁
f : M →ₗ[R] N
g : N →ₗ[R] P
f' : M' →ₗ[R] N'
g' : N' →ₗ[R] P'
φ : M₁ →ₗ[R] M ⊗[R] M'
rw : (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ
⊢ g ⊗ₘ g' ∘ₗ f ⊗ₘ f' ∘ₗ φ = (g ∘ₗ f) ⊗ₘ (g' ∘ₗ f') ∘ₗ φ
have rw₁ : (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ = (g ⊗ₘ g' ∘ₗ f ⊗ₘ f') ∘ₗ φ
Tactic: rw [← LinearMap.comp_assoc, TensorProduct.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
have rw : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
rw : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
have rw₁ : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
rw : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
rw₁ : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
have rw₂ : (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq]