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
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)
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) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
  ((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)
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)
hl₇ :
  Eq (α := A →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inl R A B) ∘ₗ (TensorProduct.mk R R A : (a : R) → A →ₗ[R] R ⊗[R] A) 1)
    ((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.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ 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
⊢ 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)
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: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := 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)
⊢ 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)
have hr₁ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₂ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₃ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₄ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₅ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₆ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₆ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₇ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ (TensorProduct.mk R R B : (a : R) → B →ₗ[R] R ⊗[R] B) 1)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₁ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₂ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₃ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map (counit ∘ₗ inr R A B) (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₄ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (TensorProduct.map counit (inr R A B) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₅ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((lTensor R (inr R A B) ∘ₗ rTensor B counit) ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₆ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ rTensor B counit ∘ₗ comul)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
hr₇ :
  Eq (α := B →ₗ[R] R ⊗[R] (A × B)) (lTensor R (inr R A B) ∘ₗ (TensorProduct.mk R R B : (a : R) → B →ₗ[R] R ⊗[R] B) 1)
    ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
⊢ 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)
have hr₈ : Eq (α := B →ₗ[R] R ⊗[R] (A × B)) ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
  ((TensorProduct.mk R R (A × B) : (a : R) → A × B →ₗ[R] R ⊗[R] (A × B)) 1 ∘ₗ inr R A B)
Tactic: rw [comp_assoc, comul_comp_inr, ← comp_assoc, rTensor_comp_map, counit_comp_inr,
        ← lTensor_comp_rTensor, comp_assoc, rTensor_counit_comp_comul, lTensor_comp_mk]
-- 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 × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1)
have hl : Eq (α := A →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
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 × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
⊢ Eq (α := A × B →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1)
have hr : Eq (α := B →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inr R A B)
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 × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
have hl : Eq (α := A →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- 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 × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
have hl₁ : Eq (α := A →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]
-- 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 × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ comul ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
hl₁ :
  Eq (α := A →ₗ[R] (A × B) ⊗[R] R) (lTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
⊢ Eq (α := A →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ comul) ∘ₗ inl R A B)
    ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
have hl₂ : Eq (α := A →ₗ[R] (A × B) ⊗[R] R) ((lTensor (A × B) counit ∘ₗ TensorProduct.map (inl R A B) (inl R A B)) ∘ₗ comul)
  ((LinearMap.flip (TensorProduct.mk R (A × B) R) : (a : R) → A × B →ₗ[R] (A × B) ⊗[R] R) 1 ∘ₗ inl R A B)
Tactic: rw [comp_assoc, comul_comp_inl, ← comp_assoc, lTensor_comp_map, counit_comp_inl,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]