awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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 : CoalgebraStruct R B
inst_10 : CoalgebraStruct S A
x : A
y : B
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B))
    ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (x ⊗ₜ[R] y) : 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))
        ((comul : (a : A) → A ⊗[S] A) x ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) y) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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 : CoalgebraStruct R B
inst_10 : CoalgebraStruct S A
x : A
y : B
⊢ (counit : (a : A ⊗[R] B) → S) (x ⊗ₜ[R] y) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((counit : (a : B) → R) y : R) ((counit : (a : A) → S) x : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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)))
⊢ 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)

Tactic:
ext x y
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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)))
⊢ Eq (α := 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)))
        ((TensorProduct.assoc S A A A : (a : A ⊗[S] A ⊗[S] A) → A ⊗[S] (A ⊗[S] A))
            ((LinearMap.rTensor A comul : (a : A ⊗[S] A) → A ⊗[S] A ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x)) ⊗ₜ[R]
          (TensorProduct.assoc R B B B : (a : B ⊗[R] B ⊗[R] B) → B ⊗[R] (B ⊗[R] B))
            ((LinearMap.rTensor B comul : (a : B ⊗[R] B) → B ⊗[R] B ⊗[R] B) ((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)))
        ((LinearMap.lTensor A comul : (a : A ⊗[S] A) → A ⊗[S] (A ⊗[S] A)) ((comul : (a : A) → A ⊗[S] A) x) ⊗ₜ[R]
          (LinearMap.lTensor B comul : (a : B ⊗[R] B) → B ⊗[R] (B ⊗[R] B)) ((comul : (a : B) → B ⊗[R] B) y)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))

Tactic:
congr(F ($(Coalgebra.coassoc_apply x) ⊗ₜ[R] $(Coalgebra.coassoc_apply y)))

Premises used: congrArg, id, congr, Coalgebra.coassoc_apply, TensorProduct.tmul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
y₁₁ y₁₂ : B
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))
    ((TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B) :
          (a : A ⊗[R] B ⊗[S] (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₁₂)) ⊗ₜ[S]
          (x₂ ⊗ₜ[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)))
        ((TensorProduct.assoc S A A A : (a : A ⊗[S] A ⊗[S] A) → A ⊗[S] (A ⊗[S] A)) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[S] x₂) ⊗ₜ[R]
          (TensorProduct.assoc R B B B : (a : B ⊗[R] B ⊗[R] B) → B ⊗[R] (B ⊗[R] B)) (y₁₁ ⊗ₜ[R] y₁₂ ⊗ₜ[R] y₂)) :
      A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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)))
⊢ 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)))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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)))
⊢ 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:
hopf_tensor_induction comul (R := S) x₂ with x₂₁ x₂₂

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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)))
⊢ 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 := R) y₂ with y₂₁ y₂₂

Premises used: CoalgebraStruct.comul, DFunLike.coe
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
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))
⊢ 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)

Tactic:
ext x y
-- Module: Mathlib.RingTheory.Coalgebra.TensorProduct
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
⊢ Eq (α := S ⊗[S] (A ⊗[R] B))
    ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A)
            ((LinearMap.rTensor A counit : (a : A ⊗[S] A) → S ⊗[S] A) ((comul : (a : A) → A ⊗[S] A) x) : S ⊗[S] A) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B)
            ((LinearMap.rTensor B counit : (a : B ⊗[R] B) → R ⊗[R] B) ((comul : (a : B) → B ⊗[R] B) y) : R ⊗[R] B)) :
      S ⊗[S] (A ⊗[R] B))
    ((LinearEquiv.symm (TensorProduct.lid S (A ⊗[R] B)) : (a : A ⊗[R] B) → S ⊗[S] (A ⊗[R] B))
        ((TensorProduct.lid S A : (a : S ⊗[S] A) → A) (1 ⊗ₜ[S] x) ⊗ₜ[R]
          (TensorProduct.lid R B : (a : R ⊗[R] B) → B) (1 ⊗ₜ[R] y)) :
      S ⊗[S] (A ⊗[R] B))

Tactic:
congr((TensorProduct.lid S _).symm
        (TensorProduct.lid _ _ $(rTensor_counit_comul (R := S) x) ⊗ₜ[R]
          TensorProduct.lid _ _ $(rTensor_counit_comul (R := R) y)))

Premises used: LinearEquiv.symm, congrArg, id, congr, Coalgebra.rTensor_counit_comul, TensorProduct.lid, TensorProduct, TensorProduct.tmul, DFunLike.coe