awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ LinearMap.rTensor A counit ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) LinearMap.id
have this₁ : Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul)
  (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
Tactic: rw [LinearMap.rTensor, ← LinearMap.comp_assoc, TensorProduct.lift_comp_map, LinearMap.compl₂_id]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
this :
  Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul)
    (TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
⊢ Eq (α := A →ₗ[R] A) (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) LinearMap.id
have h : ∀ (x : A),
  Eq (α := A) ((TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul : (a : A) → A) x : A)
    ((LinearMap.id : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₗ[R] R ⊗[R] R)
    (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
    ((TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
have h : Eq (α := R ⊗[R] R)
  ((LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
  (((TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₗ[R] R ⊗[R] R)
    (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
    ((LinearMap.flip (TensorProduct.mk R R R) : (a : R) → R →ₗ[R] R ⊗[R] R) 1)
have h : Eq (α := R ⊗[R] R)
  ((LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
  (((LinearMap.flip (TensorProduct.mk R R R) : (a : R) → R →ₗ[R] R ⊗[R] R) 1 : (a : R) → R ⊗[R] R) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Eq (α := R →ₗ[R] R ⊗[R] R) ((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul) comul
have h : Eq (α := R ⊗[R] R) (((↑(TensorProduct.comm R R R) : R ⊗[R] R →ₗ[R] R ⊗[R] R) ∘ₗ comul : (a : R) → R ⊗[R] R) 1)
  ((comul : (a : R) → R ⊗[R] R) 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := A →ₗ[R] (A × B) ⊗[R] (A × B)) (comul ∘ₗ inl R A B) (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
have h : ∀ (x : A),
  Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inl R A B : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
    ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul : (a : A) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := B →ₗ[R] (A × B) ⊗[R] (A × B)) (comul ∘ₗ inr R A B) (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
have h : ∀ (x : B),
  Eq (α := (A × B) ⊗[R] (A × B)) ((comul ∘ₗ inr R A B : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
    ((TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul : (a : B) → (A × B) ⊗[R] (A × B)) x : (A × B) ⊗[R] (A × B))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := A × B →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B)
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul)
have hl : Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
⊢ Eq (α := A × B →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B)
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul)
have hr : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl : Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₁ : Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₂ : Eq (α := A →ₗ[R] A ⊗[R] A) comul ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₃ : Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₄ : Eq (α := A →ₗ[R] A ⊗[R] A) comul
  (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₅ : Eq (α := A →ₗ[R] A ⊗[R] A) comul
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
    comul)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₆ : Eq (α := A →ₗ[R] A ⊗[R] A) comul
  (TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
hl₆ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₇ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
hl₆ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul)
hl₇ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₈ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (LinearMap.id ∘ₗ comul)
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 ⊗[R] A) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] A ⊗[R] A) (comul ∘ₗ LinearMap.id)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ
      TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
hl₅ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ
      comul)
hl₆ :
  Eq (α := A →ₗ[R] A ⊗[R] A) comul
    (TensorProduct.map (LinearMap.fst R A B ∘ₗ inl R A B) (LinearMap.fst R A B ∘ₗ inl R A B) ∘ₗ comul)
hl₇ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul)
hl₈ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul (LinearMap.id ∘ₗ comul)
⊢ Eq (α := A →ₗ[R] A ⊗[R] A) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inl R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inl R A B)
have hl₉ : Eq.{v + 1} (α := A →ₗ[R] A ⊗[R] A) comul comul
Tactic: rw [comp_assoc, fst_comp_inl, comp_id, comp_assoc, comul_comp_inl, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inl, TensorProduct.map_id, id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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
⊢ Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
have hr : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
Tactic: rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
⊢ Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
have hr₁ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ 0)
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
Tactic: rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₁ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ 0)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
⊢ Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
have hr₂ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
  ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
Tactic: rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Basic (goal)
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 (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ LinearMap.fst R A B ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₁ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) (comul ∘ₗ 0)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
hr₂ :
  Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
⊢ Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) ((comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B)
    ((TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B)
have hr₃ : Eq (α := LinearMap.{u, u, w, v} (RingHom.id R) B (A ⊗[R] A)) 0
  (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inr R A B)
Tactic: rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]