awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.Hom (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
a : A
repr : Repr.{u, v, u_2} R a
F : Type u_1
inst_7 : FunLike F A B
inst_8 : CoalgHomClass F R A B
φ : F
⊢ Eq.{w + 1} (α := B ⊗[R] B)
    (((map (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
                (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) ∘ₗ
              comul :
            LinearMap.{u, u, v, w} (RingHom.id R) A (B ⊗[R] B)) :
          (a : A) → B ⊗[R] B)
        a :
      B ⊗[R] B)
    (∑ i ∈ repr.index, ((⇑φ : (a : A) → B) ∘ repr.left) i ⊗ₜ[R] ((⇑φ : (a : A) → B) ∘ repr.right) i : B ⊗[R] B)
have rw : Eq.{w + 1} (α := B ⊗[R] B)
  (∑ x ∈ repr.index,
    ((map (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B)
            (↑φ : [inst_9 : FunLike F A B] → [SemilinearMapClass F (RingHom.id R) A B] → A →ₗ[R] B) :
          LinearMap.{u, u, v, w} (RingHom.id R) (A ⊗[R] A) (B ⊗[R] B)) :
        (a : A ⊗[R] A) → B ⊗[R] B)
      (repr.left x ⊗ₜ[R] repr.right x))
  (∑ i ∈ repr.index, ((⇑φ : (a : A) → B) ∘ repr.left) i ⊗ₜ[R] ((⇑φ : (a : A) → B) ∘ repr.right) i)
Tactic: rw [LinearMap.comp_apply, ← repr.eq, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.MulOpposite (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
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ᵐᵒᵖ)) ∘ₗ
            rTensor Aᵐᵒᵖ comul ∘ₗ comul :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ comul ∘ₗ comul : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) x : Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
have rw : Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  (((↑(TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ) : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)) ∘ₗ
          (rTensor Aᵐᵒᵖ (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
              rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
            map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
        (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      x :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  ((lTensor Aᵐᵒᵖ
            (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
          map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
            comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
        (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      x :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
Tactic: rw [comul_def, rTensor_comp, rTensor_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.MulOpposite (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
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ᵐᵒᵖ)) ∘ₗ
            (rTensor Aᵐᵒᵖ (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
                rTensor Aᵐᵒᵖ comul ∘ₗ rTensor Aᵐᵒᵖ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((lTensor Aᵐᵒᵖ
              (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
            map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        x :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
have simp : Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  ((TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ : (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      ((map (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) LinearMap.id :
          (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
        ((map comul LinearMap.id : (a : A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
          ((map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) LinearMap.id :
              (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → A ⊗[R] Aᵐᵒᵖ)
            ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
                (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
              ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))))) :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
          ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
            (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
        (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
Tactic: simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_map, rTensor_def]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.MulOpposite (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ : (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((map (map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) LinearMap.id :
            (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
          ((map comul LinearMap.id : (a : A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
            ((map (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) LinearMap.id :
                (a : Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ) → A ⊗[R] Aᵐᵒᵖ)
              ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
                  (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ)
                ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))))) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
    ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
            ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ
                comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A)) ∘ₗ
              (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
          (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
        ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
      Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
have simp_rw : Eq (α := Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  ((lTensor Aᵐᵒᵖ (lTensor Aᵐᵒᵖ LinearMap.id ∘ₗ rTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
          rTensor (A ⊗[R] Aᵐᵒᵖ) (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
        (a : A ⊗[R] (A ⊗[R] Aᵐᵒᵖ)) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ : (a : A ⊗[R] A ⊗[R] Aᵐᵒᵖ) → A ⊗[R] (A ⊗[R] Aᵐᵒᵖ))
        ((lTensor (A ⊗[R] A) (LinearMap.id ∘ₗ LinearMap.id ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
              rTensor A
                (comul ∘ₗ
                  (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
            (a : A ⊗[R] A) → A ⊗[R] A ⊗[R] Aᵐᵒᵖ)
          ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)))) :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
  ((lTensor Aᵐᵒᵖ
            ((lTensor Aᵐᵒᵖ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) ∘ₗ rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
              comul ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) ∘ₗ
          rTensor A (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
        (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
      ((comul : (a : A) → A ⊗[R] A) ((LinearEquiv.symm (opLinearEquiv R) : (a : Aᵐᵒᵖ) → A) x)) :
    Aᵐᵒᵖ ⊗[R] (Aᵐᵒᵖ ⊗[R] Aᵐᵒᵖ))
Tactic: simp_rw [← map_map_assoc, map_map, comp_assoc, ← lTensor_comp_rTensor]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.MulOpposite (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    ((rTensor Aᵐᵒᵖ counit ∘ₗ comul : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x : TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
    (((TensorProduct.mk R R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ →ₗ[R] R ⊗[R] Aᵐᵒᵖ) 1 : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x :
      TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
have simp : Eq (α := TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
  ((map (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ))
          (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ) :
        (a : A ⊗[R] A) → R ⊗[R] Aᵐᵒᵖ)
      ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
    TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
  (((TensorProduct.mk R R Aᵐᵒᵖ : (a : R) → Aᵐᵒᵖ →ₗ[R] R ⊗[R] Aᵐᵒᵖ) 1 : (a : Aᵐᵒᵖ) → R ⊗[R] Aᵐᵒᵖ) x :
    TensorProduct.{u_1, u_1, u_2} R R Aᵐᵒᵖ)
Tactic: simp only [counit_def, comul_def, coe_comp, Function.comp_apply, rTensor_map, comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.MulOpposite (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Coalgebra R A
x : Aᵐᵒᵖ
⊢ Eq (α := TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    ((lTensor Aᵐᵒᵖ counit ∘ₗ comul : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x : TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
    (((LinearMap.flip (TensorProduct.mk R Aᵐᵒᵖ R) : (a : R) → Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] R) 1 : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x :
      TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
have simp : Eq (α := TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
  ((map (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)
          (counit ∘ₗ (↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) ∘ₗ (↑(opLinearEquiv R) : A →ₗ[R] Aᵐᵒᵖ)) :
        (a : A ⊗[R] A) → Aᵐᵒᵖ ⊗[R] R)
      ((comul : (a : A) → A ⊗[R] A) (((↑(LinearEquiv.symm (opLinearEquiv R)) : Aᵐᵒᵖ →ₗ[R] A) : (a : Aᵐᵒᵖ) → A) x)) :
    TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
  (((LinearMap.flip (TensorProduct.mk R Aᵐᵒᵖ R) : (a : R) → Aᵐᵒᵖ →ₗ[R] Aᵐᵒᵖ ⊗[R] R) 1 : (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] R) x :
    TensorProduct.{u_1, u_2, u_1} R Aᵐᵒᵖ R)
Tactic: simp only [counit_def, comul_def, coe_comp, Function.comp_apply, lTensor_map, comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
⊢ Eq (α := A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) :
        A ⊗[R] B ⊗[S] (A ⊗[R] B) ⊗[S] (A ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) ∘ₗ
      LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul)
    (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul)
have a : ∀ (x : A) (y : B),
  Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (((((AlgebraTensorModule.curry
                    ((↑(TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B)) :
                        A ⊗[R] B ⊗[S] (A ⊗[R] B) ⊗[S] (A ⊗[R] B) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) ∘ₗ
                      LinearMap.rTensor (A ⊗[R] B) comul ∘ₗ comul) :
                  A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) :
          (a : B) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        y :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (((((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul) :
                  A →ₗ[S] B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) :
                (a : A) → B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
              x :
            B →ₗ[R] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B))) :
          (a : B) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        y :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
Tactic: ext x y
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
x : A
y : B
F : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  (AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) :
      TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
        A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) ≪≫ₗ
    (AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
        (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) :
      A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S]
        A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
F' : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) →ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ
      (↑F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
x₁ x₂ : A
y₁ y₂ : B
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((LinearMap.lTensor (A ⊗[R] B) comul : (a : A ⊗[R] B ⊗[S] (A ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        (((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₁ ⊗ₜ[S] x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] y₂))) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        ((LinearMap.lTensor A comul : (a : A ⊗[S] A) → A ⊗[S] (A ⊗[S] A)) (x₁ ⊗ₜ[S] x₂) ⊗ₜ[R]
          (LinearMap.lTensor B comul : (a : B ⊗[R] B) → B ⊗[R] (B ⊗[R] B)) (y₁ ⊗ₜ[R] y₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
have h : Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
  (x₁ ⊗ₜ[R] y₁ ⊗ₜ[S]
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
          (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
        ((comul : (a : A) → A ⊗[S] A) x₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂) :
    A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
  ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
      (x₁ ⊗ₜ[S] (comul : (a : A) → A ⊗[S] A) x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂)) :
    A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
x : A
y : B
F : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  (AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) :
      TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
        A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) ≪≫ₗ
    (AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
        (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) :
      A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S]
        A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
F' : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) →ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ
      (↑F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
x₁ x₂ : A
y₁ y₂ : B
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (x₁ ⊗ₜ[R] y₁ ⊗ₜ[S]
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          ((comul : (a : A) → A ⊗[S] A) x₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        (x₁ ⊗ₜ[S] (comul : (a : A) → A ⊗[S] A) x₂ ⊗ₜ[R] (y₁ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
have h : ∀ (x₂₁ x₂₂ : A),
  Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (x₁ ⊗ₜ[R] y₁ ⊗ₜ[S]
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₂₁ ⊗ₜ[S] x₂₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        (x₁ ⊗ₜ[S] (x₂₁ ⊗ₜ[S] x₂₂) ⊗ₜ[R] (y₁ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
Tactic: hopf_tensor_induction comul (R := S) x₂ with x₂₁ x₂₂
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
x : A
y : B
F : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  (AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) :
      TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S]
        A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) ≪≫ₗ
    (AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
        (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) :
      A ⊗[R] B ⊗[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S]
        A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
F' : TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] (A ⊗[S] A)) (B ⊗[R] (B ⊗[R] B)) →ₗ[S]
  A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ
      (↑F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
x₁ x₂ : A
y₁ y₂ : B
x₂₁ x₂₂ : A
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (x₁ ⊗ₜ[R] y₁ ⊗ₜ[S]
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₂₁ ⊗ₜ[S] x₂₂ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        (x₁ ⊗ₜ[S] (x₂₁ ⊗ₜ[S] x₂₂) ⊗ₜ[R] (y₁ ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
have h : ∀ (y₂₁ y₂₂ : B),
  Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    (x₁ ⊗ₜ[R] y₁ ⊗ₜ[S]
        ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B :
              TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
            (a : A ⊗[S] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (x₂₁ ⊗ₜ[S] x₂₂ ⊗ₜ[R] (y₂₁ ⊗ₜ[R] y₂₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((F : (a : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B))) → A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
        (x₁ ⊗ₜ[S] (x₂₁ ⊗ₜ[S] x₂₂) ⊗ₜ[R] (y₁ ⊗ₜ[R] (y₂₁ ⊗ₜ[R] y₂₂))) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
Tactic: hopf_tensor_induction comul (R := R) y₂ with y₂₁ y₂₂
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid A
inst_3 : AddCommMonoid B
inst_4 : Algebra R S
inst_5 : Module R A
inst_6 : Module S A
inst_7 : Module R B
inst_8 : IsScalarTower R S A
inst_9 : Coalgebra R B
inst_10 : Coalgebra S A
⊢ Eq (α := A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul)
    ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1)
have a : ∀ (x : A) (y : B),
  Eq (α := S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul) : A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
    (((((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B) : (a : S) → A ⊗[R] B →ₗ[S] S ⊗[S] (A ⊗[R] B)) 1) :
                  A →ₗ[S] B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
                (a : A) → B →ₗ[R] S ⊗[S] (A ⊗[R] B))
              x :
            B →ₗ[R] S ⊗[S] (A ⊗[R] B)) :
          (a : B) → S ⊗[S] (A ⊗[R] B))
        y :
      S ⊗[S] (A ⊗[R] B))
Tactic: ext x y