awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : A
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
                (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B))) ∘ₗ
              rTensor (A × B)
                  (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                    (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
                coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inl R A B :
          (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    (((lTensor (A × B)
                (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
              coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inl R A B :
          (a : A) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
have hl : Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
        (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((rTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) x) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) 0) :
            (A × B) ⊗[R] (A × B)))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((lTensor (A × B)
          (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
        (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
            ((comul : (a : A) → A ⊗[R] A) x) :
          (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
            ((comul : (a : B) → B ⊗[R] B) 0) :
          (A × B) ⊗[R] (A × B))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]
-- 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
x : B
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((((↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) :
                (A × B) ⊗[R] (A × B) ⊗[R] (A × B) →ₗ[R] (A × B) ⊗[R] ((A × B) ⊗[R] (A × B))) ∘ₗ
              rTensor (A × B)
                  (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                    (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
                coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inr R A B :
          (a : B) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    (((lTensor (A × B)
                (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                  (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
              coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) ∘ₗ
            inr R A B :
          (a : B) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        x :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
have hr : Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
        (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((rTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) 0) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) x) :
            (A × B) ⊗[R] (A × B)))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((lTensor (A × B)
          (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
        (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
            ((comul : (a : A) → A ⊗[R] A) 0) :
          (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
            ((comul : (a : B) → B ⊗[R] B) x) :
          (A × B) ⊗[R] (A × B))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: dsimp only [comp_apply, LinearEquiv.coe_coe, coe_inl, coe_inr, coprod_apply]
-- 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
x : A
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
                ((comul : (a : A) → A ⊗[R] A) x) :
              (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
                ((comul : (a : B) → B ⊗[R] B) 0) :
              (A × B) ⊗[R] (A × B)))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) x) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) 0) :
            (A × B) ⊗[R] (A × B))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
have hl : Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
        (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((rTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
          ((comul : (a : A) → A ⊗[R] A) x))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((lTensor (A × B)
          (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
        (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
        ((comul : (a : A) → A ⊗[R] A) x)) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: simp only [map_zero, add_zero]
-- 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
x : B
⊢ Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
          (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        ((rTensor (A × B)
              (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
                (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
            (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
          (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
                ((comul : (a : A) → A ⊗[R] A) 0) :
              (A × B) ⊗[R] (A × B))
            ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
                ((comul : (a : B) → B ⊗[R] B) x) :
              (A × B) ⊗[R] (A × B)))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
    ((lTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
        (HAdd.hAdd (α := (A × B) ⊗[R] (A × B)) (β := (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inl R A B) (inl R A B) : (a : A ⊗[R] A) → (A × B) ⊗[R] (A × B))
              ((comul : (a : A) → A ⊗[R] A) 0) :
            (A × B) ⊗[R] (A × B))
          ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
              ((comul : (a : B) → B ⊗[R] B) x) :
            (A × B) ⊗[R] (A × B))) :
      (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
have hr : Eq (α := (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((TensorProduct.assoc R (A × B) (A × B) (A × B) :
        (a : (A × B) ⊗[R] (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((rTensor (A × B)
            (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
              (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
          (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] (A × B) ⊗[R] (A × B))
        ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
          ((comul : (a : B) → B ⊗[R] B) x))) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
  ((lTensor (A × B)
          (coprod (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)) :
        (a : (A × B) ⊗[R] (A × B)) → (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
      ((TensorProduct.map (inr R A B) (inr R A B) : (a : B ⊗[R] B) → (A × B) ⊗[R] (A × B))
        ((comul : (a : B) → B ⊗[R] B) x)) :
    (A × B) ⊗[R] ((A × B) ⊗[R] (A × B)))
Tactic: simp only [map_zero, zero_add]
-- 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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1)
have hl : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ 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] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A × B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1)
have 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)
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] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₁ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₂ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₃ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₄ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inl R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₅ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inl R A B) ∘ₗ rTensor A counit) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← 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
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] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₂ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₃ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inl R A B) (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₄ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inl R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
hl₅ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inl R A B) ∘ₗ rTensor A counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
have hl₆ : Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inl R A B) ∘ₗ rTensor A counit ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, rTensor_comp_map, counit_comp_inl,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]