awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Equiv (goal)
Goal:
R : Type u
A : Type v
B : Type w
C : Type u₁
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Bialgebra R A
inst_4 : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective.{v + 1, w + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ AlgHom.comp
      (Algebra.TensorProduct.map (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
          (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) :
        AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
      (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) =
    AlgHom.comp (comulAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
have H : ∀ (x : A),
  Eq.{w + 1} (α := B ⊗[R] B)
    (((AlgHom.comp
              (Algebra.TensorProduct.map (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B)
                  (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) :
                AlgHom.{u, v, w} R (A ⊗[R] A) (B ⊗[R] B))
              (comulAlgHom R A : A →ₐ[R] A ⊗[R] A) :
            AlgHom.{u, v, w} R A (B ⊗[R] B)) :
          (a : A) → B ⊗[R] B)
        x :
      B ⊗[R] B)
    ((AlgHom.comp (comulAlgHom R B) (↑(AlgEquiv.ofBijective (↑f : A →ₐ[R] B) hf) : A →ₐ[R] B) : (a : A) → B ⊗[R] B) x :
      B ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
f g : A →ₐc[R] B
h : Eq (α := (a : A) → B) ((fun (f : A →ₐc[R] B) ↦ f.toFun) f) ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)
⊢ f = g
have rcases : ∀ (toCoalgHom : A →ₗc[R] B) (map_one' : toCoalgHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y)
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)),
  { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } = g
Tactic: rcases f with ⟨_, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : CoalgebraStruct R A
inst_10 : CoalgebraStruct R B
inst_11 : CoalgebraStruct R C
inst_12 : CoalgebraStruct R D
g : A →ₐc[R] B
toCoalgHom : A →ₗc[R] B
map_one' : toCoalgHom.toFun 1 = 1
map_mul' : ∀ (x y : A), toCoalgHom.toFun (x * y) = toCoalgHom.toFun x * toCoalgHom.toFun y
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
    ((fun (f : A →ₐc[R] B) ↦ f.toFun) g)
⊢ { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } = g
have rcases : ∀ (toCoalgHom_1 : A →ₗc[R] B) (map_one'_1 : toCoalgHom_1.toFun 1 = 1)
  (map_mul'_1 : ∀ (x y : A), toCoalgHom_1.toFun (x * y) = toCoalgHom_1.toFun x * toCoalgHom_1.toFun y)
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : A →ₐc[R] B) ↦ f.toFun) { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' })
      ((fun (f : A →ₐc[R] B) ↦ f.toFun)
        { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 })),
  { toCoalgHom := toCoalgHom, map_one' := map_one', map_mul' := map_mul' : A →ₐc[R] B } =
    { toCoalgHom := toCoalgHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }
Tactic: rcases g with ⟨_, _⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.Hom (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : CoalgebraStruct R A
f g : R →ₐc[R] A
h : Eq.{u_2 + 1} (α := A) ((f : (a : R) → A) 1 : A) ((g : (a : R) → A) 1 : A)
⊢ Eq (α := R →ₗ[R] A)
    ((fun (x : R →ₐc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₐc[R] A) R A] → [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      f)
    ((fun (x : R →ₐc[R] A) ↦
        ((↑x : [inst_4 : FunLike (R →ₐc[R] A) R A] → [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
          R →ₗ[R] A))
      g)
have h₁ : Eq.{u_2 + 1} (α := A)
  (((fun (x : R →ₐc[R] A) ↦
            ((↑x :
                [inst_4 : FunLike (R →ₐc[R] A) R A] →
                  [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
              R →ₗ[R] A))
          f :
        (a : R) → A)
      1 :
    A)
  (((fun (x : R →ₐc[R] A) ↦
            ((↑x :
                [inst_4 : FunLike (R →ₐc[R] A) R A] →
                  [SemilinearMapClass (R →ₐc[R] A) (RingHom.id R) R A] → R →ₗ[R] A) :
              R →ₗ[R] A))
          g :
        (a : R) → A)
      1 :
    A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
⊢ Eq (α := A[M] →ₗ[R] A[M] →ₗ[R] R) (LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.counit)
    (LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit)
have H : ∀ (x : M) (x_1 : A) (x_2 : M) (x_3 : A),
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.counit ∘ₗ lsingle x : (a : A) → A[M] →ₗ[R] R) x_1 ∘ₗ
            lsingle x_2 :
          (a : A) → R)
        x_3 :
      R)
    (((LinearMap.compl₁₂ (LinearMap.mul R R) CoalgebraStruct.counit CoalgebraStruct.counit ∘ₗ lsingle x :
                (a : A) → A[M] →ₗ[R] R)
              x_1 ∘ₗ
            lsingle x_2 :
          (a : A) → R)
        x_3 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
⊢ Eq (α := A[M] →ₗ[R] A[M] →ₗ[R] TensorProduct R A[M] A[M])
    (LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.comul)
    (LinearMap.compl₁₂ (LinearMap.mul R (TensorProduct R A[M] A[M])) CoalgebraStruct.comul CoalgebraStruct.comul)
have H : ∀ (a : M) (b : A) (c : M) (d : A),
  Eq (α := TensorProduct R A[M] A[M])
    (((LinearMap.compr₂ (LinearMap.mul R A[M]) CoalgebraStruct.comul ∘ₗ lsingle a :
                (a : A) → A[M] →ₗ[R] TensorProduct R A[M] A[M])
              b ∘ₗ
            lsingle c :
          (a : A) → TensorProduct R A[M] A[M])
        d :
      TensorProduct R A[M] A[M])
    (((LinearMap.compl₁₂ (LinearMap.mul R (TensorProduct R A[M] A[M])) CoalgebraStruct.comul CoalgebraStruct.comul ∘ₗ
                  lsingle a :
                (a : A) → A[M] →ₗ[R] TensorProduct R A[M] A[M])
              b ∘ₗ
            lsingle c :
          (a : A) → TensorProduct R A[M] A[M])
        d :
      TensorProduct R A[M] A[M])
Tactic: ext a b c d
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
inst_6 : AddMonoid M
inst_7 : AddMonoid N
f : M →+ N
⊢ Eq (α := AddMonoidAlgebra R M →ₐ[R] R)
    (AlgHom.comp (counitAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f))
    (counitAlgHom R (AddMonoidAlgebra R M))
have h : ∀ (x : M),
  Eq.{u_1 + 1} (α := R)
    ((Additive.toMul : (a : Additive R) → R)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* R) → M →+ Additive R)
                  (MonoidHom.comp
                    (↑(AlgHom.comp (counitAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f)) :
                      AddMonoidAlgebra R M →* R)
                    (AddMonoidAlgebra.of R M)) :
                AddMonoidHom.{u_3, u_1} M (Additive R)) :
              (a : M) → Additive R)
            x :
          Additive R) :
      R)
    ((Additive.toMul : (a : Additive R) → R)
        ((((MonoidHom.toAdditiveRight : (a : Multiplicative M →* R) → M →+ Additive R)
                  (MonoidHom.comp (↑(counitAlgHom R (AddMonoidAlgebra R M)) : AddMonoidAlgebra R M →* R)
                    (AddMonoidAlgebra.of R M)) :
                AddMonoidHom.{u_3, u_1} M (Additive R)) :
              (a : M) → Additive R)
            x :
          Additive R) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
f : M →* N
⊢ Eq (α := R[M] →ₐ[R] R) (AlgHom.comp (counitAlgHom R R[N]) (mapDomainAlgHom R R f)) (counitAlgHom R R[M])
have h : ∀ (x : M),
  Eq.{u_1 + 1} (α := R)
    ((MonoidHom.comp (↑(AlgHom.comp (counitAlgHom R R[N]) (mapDomainAlgHom R R f)) : R[M] →* R) (of R M) : (a : M) → R)
        x :
      R)
    ((MonoidHom.comp (↑(counitAlgHom R R[M]) : R[M] →* R) (of R M) : (a : M) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Bialgebra R A
inst_3 : Monoid M
inst_4 : Monoid N
inst_5 : Monoid O
f : M →* N
⊢ Eq (α := R[M] →ₐ[R] TensorProduct R R[N] R[N])
    (AlgHom.comp
        (Algebra.TensorProduct.map (mapDomainAlgHom R R f) (mapDomainAlgHom R R f) :
          TensorProduct R R[M] R[M] →ₐ[R] TensorProduct R R[N] R[N])
        (comulAlgHom R R[M] : R[M] →ₐ[R] TensorProduct R R[M] R[M]) :
      R[M] →ₐ[R] TensorProduct R R[N] R[N])
    (AlgHom.comp (comulAlgHom R R[N]) (mapDomainAlgHom R R f) : R[M] →ₐ[R] TensorProduct R R[N] R[N])
have h : ∀ (x : M),
  Eq (α := TensorProduct R R[N] R[N])
    ((MonoidHom.comp
            (↑(AlgHom.comp
                    (Algebra.TensorProduct.map (mapDomainAlgHom R R f) (mapDomainAlgHom R R f) :
                      TensorProduct R R[M] R[M] →ₐ[R] TensorProduct R R[N] R[N])
                    (comulAlgHom R R[M] : R[M] →ₐ[R] TensorProduct R R[M] R[M]) :
                  R[M] →ₐ[R] TensorProduct R R[N] R[N]) :
              R[M] →* TensorProduct R R[N] R[N])
            (of R M) :
          (a : M) → TensorProduct R R[N] R[N])
        x :
      TensorProduct R R[N] R[N])
    ((MonoidHom.comp (↑(AlgHom.comp (comulAlgHom R R[N]) (mapDomainAlgHom R R f)) : R[M] →* TensorProduct R R[N] R[N])
            (of R M) :
          (a : M) → TensorProduct R R[N] R[N])
        x :
      TensorProduct R R[N] R[N])
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : Monoid M
⊢ Eq (α := R[M] →ₐc[R] R[M]) (mapDomainBialgHom R (MonoidHom.id M)) (BialgHom.id R R[M])
have H : ∀ (x : R[M]) (m : M),
  Eq.{u_1 + 1} (α := R) ((((mapDomainBialgHom R (MonoidHom.id M) : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
    ((((BialgHom.id R R[M] : (a : R[M]) → R[M]) x : R[M]) : (a : M) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
f : N →* O
g : M →* N
⊢ Eq (α := R[M] →ₐc[R] R[O]) (mapDomainBialgHom R (f.comp g))
    (BialgHom.comp (mapDomainBialgHom R f) (mapDomainBialgHom R g))
have H : ∀ (x : R[M]) (m : O),
  Eq.{u_1 + 1} (α := R) ((((mapDomainBialgHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
    ((((BialgHom.comp (mapDomainBialgHom R f) (mapDomainBialgHom R g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.MonoidAlgebra (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
O : Type u_5
inst : CommSemiring R
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Monoid O
f : N →* O
g : M →* N
x : R[M]
⊢ Eq (α := R[O]) ((mapDomainBialgHom R f : (a : R[N]) → R[O]) ((mapDomainBialgHom R g : (a : R[M]) → R[N]) x) : R[O])
    ((mapDomainBialgHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O])
have hfg : ∀ (m : O),
  Eq.{u_1 + 1} (α := R)
    ((((mapDomainBialgHom R f : (a : R[N]) → R[O]) ((mapDomainBialgHom R g : (a : R[M]) → R[N]) x) : R[O]) :
          (a : O) → R)
        m :
      R)
    ((((mapDomainBialgHom R (f.comp g) : (a : R[M]) → R[O]) x : R[O]) : (a : O) → R) m : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.SymmetricAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (AlgHom.comp
      (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))
have h : ∀ (x : M),
  Eq (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(AlgHom.comp
                  (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                    SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.SymmetricAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(AlgHom.comp
                  (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                    SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (((↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (RingHom.id R) (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        x :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
have h : HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) =
  HAdd.hAdd (α := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) (β := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    ((ι R M : (a : M) → SymmetricAlgebra R M) x ⊗ₜ[R] 1 : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (1 ⊗ₜ[R] (ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.SymmetricAlgebra (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    ((↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) ∘ₗ
      CoalgebraStruct.comul)
    CoalgebraStruct.comul
have h : Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
  (AlgHom.comp
    (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
    (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)))
  (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))
Tactic: have h : (Algebra.TensorProduct.comm R (SymmetricAlgebra R M)
          (SymmetricAlgebra R M)).toAlgHom.comp (Bialgebra.comulAlgHom R _) =
        Bialgebra.comulAlgHom R (SymmetricAlgebra R M) := by
      ext x
      simp
      abel
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (hypothesis)
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
⊢ Bialgebra S (A ⊗[R] B)
have 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)
Tactic: have hcounit := congr(DFunLike.coe $(counit_eq_algHom_toLinearMap R S A B))
-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.TensorProduct (hypothesis)
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)
⊢ Bialgebra S (A ⊗[R] B)
have 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))
Tactic: have hcomul := congr(DFunLike.coe $(comul_eq_algHom_toLinearMap R S A B))
-- 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))
⊢ Bialgebra S (A ⊗[R] B)
have refine_1 : Eq.{u_2 + 1} (α := S) ((counit : (a : A ⊗[R] B) → S) 1 : S) (1 : S)
Tactic: refine Bialgebra.mk' S (A ⊗[R] B) ?_ (fun {x y} => ?_) ?_ (fun {x y} => ?_)