awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
refine_1 : Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
⊢ Bialgebra S (A ⊗[R] B)
have refine_2 : ∀ {x y : A ⊗[R] B},
  (counit : (a : A ⊗[R] B) → S) (x * y) =
    HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)
Tactic: refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
refine_1 : Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
refine_2 :
  ∀ {x y : A ⊗[R] B},
    (counit : (a : A ⊗[R] B) → S) (x * y) =
      HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)
⊢ Bialgebra S (A ⊗[R] B)
have refine_3 : Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) 1) 1
Tactic: refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
refine_1 : Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
refine_2 :
  ∀ {x y : A ⊗[R] B},
    (counit : (a : A ⊗[R] B) → S) (x * y) =
      HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)
refine_3 : Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) 1) 1
⊢ Bialgebra S (A ⊗[R] B)
have refine_4 : ∀ {x y : A ⊗[R] B},
  (comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (x * y) =
    HMul.hMul (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) (β := A ⊗[R] B ⊗[S] (A ⊗[R] B))
      ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) x : A ⊗[R] B ⊗[S] (A ⊗[R] B))
      ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) y : A ⊗[R] B ⊗[S] (A ⊗[R] B))
Tactic: refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
⊢ Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
have refine_1 : Eq.{u_2 + 1} (α := S)
  (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
            (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
          A ⊗[R] B →ₐ[S] S) :
        (a : A ⊗[R] B) → S)
      1 :
    S)
  (1 : S)
Tactic: simp_all only [AlgHom.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
x y : A ⊗[R] B
⊢ (counit : (a : A ⊗[R] B) → S) (x * y) =
    HMul.hMul (α := S) (β := S) ((counit : (a : A ⊗[R] B) → S) x : S) ((counit : (a : A ⊗[R] B) → S) y : S)
have refine_2 : ((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
        A ⊗[R] B →ₐ[S] S) :
      (a : A ⊗[R] B) → S)
    (x * y) =
  HMul.hMul (α := S) (β := S)
    (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
            A ⊗[R] B →ₐ[S] S) :
          (a : A ⊗[R] B) → S)
        x :
      S)
    (((AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R) :
            A ⊗[R] B →ₐ[S] S) :
          (a : A ⊗[R] B) → S)
        y :
      S)
Tactic: simp_all only [AlgHom.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra S A
inst_5 : Bialgebra R B
inst_6 : Algebra R A
inst_7 : Algebra R S
inst_8 : IsScalarTower R S A
hcounit :
  Eq (α := (a : A ⊗[R] B) → S) (⇑counit : (a : A ⊗[R] B) → S)
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := S ⊗[R] R) ((↑(Algebra.TensorProduct.rid R S S) : S ⊗[R] R →ₐ[S] S) : S ⊗[R] R →ₐ[S] S)
              (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B) : A ⊗[R] B →ₐ[S] S ⊗[R] R)) :
          A ⊗[R] B →ₗ[S] S) :
      (a : A ⊗[R] B) → S)
hcomul :
  Eq (α := (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) (⇑comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    (⇑(AlgHom.toLinearMap
            (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
              ((↑(Algebra.TensorProduct.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)) :
                TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
              (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
                A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))) :
          A ⊗[R] B →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
⊢ Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B)) ((comul : (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B)) 1) 1
have refine_3 : Eq (α := A ⊗[R] B ⊗[S] (A ⊗[R] B))
  (((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B))
          ((↑(Algebra.TensorProduct.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)) :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B) →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B))
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B) :
            A ⊗[R] B →ₐ[S] TensorProduct.{u_1, u_3, u_4} R (A ⊗[S] A) (B ⊗[R] B)) :
        A ⊗[R] B →ₐ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B)) :
      (a : A ⊗[R] B) → A ⊗[R] B ⊗[S] (A ⊗[R] B))
    1)
  1
Tactic: simp_all only [AlgHom.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Bialgebra S A
inst_4 : Algebra R A
inst_5 : Algebra R S
inst_6 : IsScalarTower R S A
⊢ Eq (α := A ⊗[R] R ≃ₐ[S] A) (BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A)
    (Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A)
have h : ∀ (x : A ⊗[R] R),
  Eq.{u_3 + 1} (α := A)
    (((BialgEquiv.toAlgEquiv (TensorProduct.rid R S A) : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
    (((Algebra.TensorProduct.rid R S A : A ⊗[R] R ≃ₐ[S] A) : (a : A ⊗[R] R) → A) x : A)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
⊢ Eq (α := A ⊗[R] B →ₐ[R] R)
    (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
    (counitAlgHom R (A ⊗[R] B))
have ha : ∀ (x : A),
  Eq.{u_1 + 1} (α := R)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
              (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
            Algebra.TensorProduct.includeLeft :
          (a : A) → R)
        x :
      R)
    ((AlgHom.comp (B := A ⊗[R] B) (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R) Algebra.TensorProduct.includeLeft :
          (a : A) → R)
        x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
ha :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := R)
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
                (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
              Algebra.TensorProduct.includeLeft :
            (a : A) → R)
          x :
        R)
      ((AlgHom.comp (B := A ⊗[R] B) (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R) Algebra.TensorProduct.includeLeft :
            (a : A) → R)
          x :
        R)
⊢ Eq (α := A ⊗[R] B →ₐ[R] R)
    (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
    (counitAlgHom R (A ⊗[R] B))
have hb : ∀ (x : B),
  Eq.{u_1 + 1} (α := R)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := B ⊗[R] A) (counitAlgHom R (B ⊗[R] A))
                (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → R)
        x :
      R)
    ((AlgHom.comp (B := A ⊗[R] B) (AlgHom.restrictScalars R (counitAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] R))
            Algebra.TensorProduct.includeRight :
          (a : B) → R)
        x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
⊢ Eq (α := A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
        (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
have ha : ∀ (a : A),
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                    (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                  A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))
              Algebra.TensorProduct.includeLeft :
            A →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
            Algebra.TensorProduct.includeLeft :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
ha :
  ∀ (a : A),
    Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((AlgHom.comp (B := A ⊗[R] B)
                (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                  (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                    A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                  (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))
                Algebra.TensorProduct.includeLeft :
              A →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
            (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
              Algebra.TensorProduct.includeLeft :
            (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
          a :
        B ⊗[R] A ⊗[R] (B ⊗[R] A))
⊢ Eq (α := A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
        (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
        (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
      A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
have hb : ∀ (a : B),
  Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                  (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                      (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                    A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                  (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
                A ⊗[R] B →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R
              (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)))
            Algebra.TensorProduct.includeRight :
          (a : B) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Bialgebra R A
inst_5 : Bialgebra R B
a : A
⊢ Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
    (((AlgHom.comp (B := A ⊗[R] B)
              (AlgHom.comp (B := A ⊗[R] B ⊗[R] (A ⊗[R] B))
                (Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
                    (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
                  A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A))
                (comulAlgHom R (A ⊗[R] B) : A ⊗[R] B →ₐ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))
              Algebra.TensorProduct.includeLeft :
            A →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.comp (comulAlgHom R (B ⊗[R] A)) (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A))
            Algebra.TensorProduct.includeLeft :
          (a : A) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
        a :
      B ⊗[R] A ⊗[R] (B ⊗[R] A))
have ha : Eq (α := B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((Algebra.TensorProduct.map (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A)
            (↑(Algebra.TensorProduct.comm R A B) : A ⊗[R] B →ₐ[R] B ⊗[R] A) :
          A ⊗[R] B ⊗[R] (A ⊗[R] B) →ₐ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : A ⊗[R] B ⊗[R] (A ⊗[R] B)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R A A B B :
            TensorProduct.{u_1, u_3, u_4} R (A ⊗[R] A) (B ⊗[R] B) ≃ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
          (a : A ⊗[R] A ⊗[R] (B ⊗[R] B)) → A ⊗[R] B ⊗[R] (A ⊗[R] B))
        ((comul : (a : A) → A ⊗[R] A) a ⊗ₜ[R] (comul : (a : B) → B ⊗[R] B) 1)) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
  (((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R R R B B A A :
          TensorProduct.{u_1, u_4, u_3} R (B ⊗[R] B) (A ⊗[R] A) ≃ₗ[R] B ⊗[R] A ⊗[R] (B ⊗[R] A)) :
        (a : B ⊗[R] B ⊗[R] (A ⊗[R] A)) → B ⊗[R] A ⊗[R] (B ⊗[R] A))
      ((comul : (a : B) → B ⊗[R] B) 1 ⊗ₜ[R] (comul : (a : A) → A ⊗[R] A) a) :
    B ⊗[R] A ⊗[R] (B ⊗[R] A))
Tactic: dsimp