awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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:
simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply,
      LinearMap.mul_apply', single_mul_single, comul_single, Bialgebra.comul_mul,
      ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq, Finset.sum_mul_sum,
      Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
      LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
      Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]

Premises used: LinearMap.mul_apply', Finset.sum_apply, LinearMap.compr₂_apply, MonoidAlgebra.lsingle_apply, Algebra.TensorProduct.tmul_mul_tmul, LinearMap.coe_sum, MonoidAlgebra.single_mul_single, map_sum, Bialgebra.comul_mul, LinearMap.coe_comp, MonoidAlgebra.comul_single, LinearMap.compl₁₂_apply, TensorProduct.map_tmul, Function.comp_apply, Finset.sum_comm, Coalgebra.Repr.eq, Coalgebra.Repr.arbitrary, Finset.sum_mul_sum
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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)
⊢ Eq (α := AddMonoidAlgebra R M →ₐ[R] R)
    (AlgHom.comp (counitAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f))
    (counitAlgHom R (AddMonoidAlgebra R M))

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
x : M
⊢ Eq (α := TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
    ((Additive.toMul :
          (a : Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) →
            TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
        ((((MonoidHom.toAdditiveRight :
                  (a : Multiplicative M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) →
                    M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
                (MonoidHom.comp
                  (↑(AlgHom.comp
                          (Algebra.TensorProduct.map (AddMonoidAlgebra.mapDomainAlgHom R R f)
                              (AddMonoidAlgebra.mapDomainAlgHom R R f) :
                            TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M) →ₐ[R]
                              TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                          (comulAlgHom R (AddMonoidAlgebra R M) :
                            AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R M)) :
                        AddMonoidAlgebra R M →ₐ[R] TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) :
                    AddMonoidAlgebra R M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                  (AddMonoidAlgebra.of R M)) :
              M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) :
            (a : M) → Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
          x) :
      TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
    ((Additive.toMul :
          (a : Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) →
            TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
        ((((MonoidHom.toAdditiveRight :
                  (a : Multiplicative M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)) →
                    M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
                (MonoidHom.comp
                  (↑(AlgHom.comp (comulAlgHom R (AddMonoidAlgebra R N)) (AddMonoidAlgebra.mapDomainAlgHom R R f)) :
                    AddMonoidAlgebra R M →* TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))
                  (AddMonoidAlgebra.of R M)) :
              M →+ Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))) :
            (a : M) → Additive (TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N)))
          x) :
      TensorProduct R (AddMonoidAlgebra R N) (AddMonoidAlgebra R N))

Tactic:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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)
⊢ Eq (α := R[M] →ₐ[R] R) (AlgHom.comp (counitAlgHom R R[N]) (mapDomainAlgHom R R f)) (counitAlgHom R R[M])

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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])
⊢ 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])

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : Monoid M
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)
⊢ Eq (α := R[M] →ₐc[R] R[M]) (mapDomainBialgHom R (MonoidHom.id M)) (BialgHom.id R R[M])

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : Monoid M
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:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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
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)
⊢ Eq (α := R[M] →ₐc[R] R[O]) (mapDomainBialgHom R (f.comp g))
    (BialgHom.comp (mapDomainBialgHom R f) (mapDomainBialgHom R g))

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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]
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:
simp [Finsupp.mapDomain_comp]

Premises used: Finsupp.mapDomain_comp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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]
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)
⊢ 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])

Tactic:
ext
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
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]
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:
simp
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_6
inst : CommSemiring R
A : Type u_7
inst_1 : Semiring A
inst_2 : Bialgebra R A
n : ℤ
⊢ Eq.{u_7 + 1} (α := TensorProduct R A[T;T⁻¹] A[T;T⁻¹])
    ((CoalgebraStruct.comul : (a : A[T;T⁻¹]) → TensorProduct R A[T;T⁻¹] A[T;T⁻¹]) (T n) :
      TensorProduct R A[T;T⁻¹] A[T;T⁻¹])
    (T n ⊗ₜ[R] T n : TensorProduct R A[T;T⁻¹] A[T;T⁻¹])

Tactic:
simp [T, -single_eq_C_mul_T, Algebra.TensorProduct.one_def]

Premises used: LaurentPolynomial.T, LaurentPolynomial.single_eq_C_mul_T, Algebra.TensorProduct.one_def
-- Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Goal:
R : Type u_6
inst : CommSemiring R
A : Type u_7
inst_1 : Semiring A
inst_2 : Bialgebra R A
n : ℤ
⊢ Eq.{u_6 + 1} (α := R) ((CoalgebraStruct.counit : (a : A[T;T⁻¹]) → R) (T n) : R) (1 : R)

Tactic:
simp [T, -single_eq_C_mul_T]

Premises used: LaurentPolynomial.T, LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := R ⊗[R] SymmetricAlgebra R M)
    (((↑(AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (Algebra.TensorProduct.map algebraMapInv (AlgHom.id R (SymmetricAlgebra R M)) :
                      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M)
                    ((lift :
                          (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                                (a : SymmetricAlgebra R M) →
                                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                              1 ∘ₗ
                            ι R M)
                          ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                                (a : SymmetricAlgebra R M) →
                                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                              1 ∘ₗ
                            ι R M)) :
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
                  SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) (SymmetricAlgebra R M)
                    (R ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) (RingHom.id R)
                      (SymmetricAlgebra R M) (R ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] R ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → R ⊗[R] SymmetricAlgebra R M)
        x :
      R ⊗[R] SymmetricAlgebra R M)
    (((↑(↑(AlgEquiv.symm (Algebra.TensorProduct.lid R (SymmetricAlgebra R M))) :
                  SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) (SymmetricAlgebra R M)
                    (R ⊗[R] SymmetricAlgebra R M)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] R ⊗[R] SymmetricAlgebra R M) (RingHom.id R)
                      (SymmetricAlgebra R M) (R ⊗[R] SymmetricAlgebra R M)] →
                  SymmetricAlgebra R M →ₗ[R] R ⊗[R] SymmetricAlgebra R M) ∘ₗ
            ι R M :
          (a : M) → R ⊗[R] SymmetricAlgebra R M)
        x :
      R ⊗[R] SymmetricAlgebra R M)

Tactic:
simp [algebraMapInv_ι]

Premises used: SymmetricAlgebra.algebraMapInv_ι
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
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] R)
    (((↑(AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv :
                      SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R)
                    ((lift :
                          (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                                (a : SymmetricAlgebra R M) →
                                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                              1 ∘ₗ
                            ι R M)
                          ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                                (a : SymmetricAlgebra R M) →
                                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                              1 ∘ₗ
                            ι R M)) :
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
                  SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (SymmetricAlgebra R M)
                    (SymmetricAlgebra R M ⊗[R] R)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (RingHom.id R)
                      (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] R)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] R) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] R)
        x :
      SymmetricAlgebra R M ⊗[R] R)
    (((↑((↑(AlgEquiv.symm (Algebra.TensorProduct.rid R R (SymmetricAlgebra R M))) :
                    SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
                  SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
              [inst_3 :
                  FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (SymmetricAlgebra R M)
                    (SymmetricAlgebra R M ⊗[R] R)] →
                [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (RingHom.id R)
                      (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] R)] →
                  SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] R) ∘ₗ
            ι R M :
          (a : M) → SymmetricAlgebra R M ⊗[R] R)
        x :
      SymmetricAlgebra R M ⊗[R] R)

Tactic:
simp [algebraMapInv_ι]

Premises used: SymmetricAlgebra.algebraMapInv_ι
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ (CoalgebraStruct.comul : (a : SymmetricAlgebra R M) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
      ((ι R M : (a : M) → SymmetricAlgebra R M) x) =
    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:
lift_ι_apply _ x

Premises used: SymmetricAlgebra.lift_ι_apply, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((CoalgebraStruct.counit : (a : SymmetricAlgebra R M) → R)
        ((ι R M : (a : M) → SymmetricAlgebra R M) x : SymmetricAlgebra R M) :
      R)
    (0 : R)

Tactic:
algebraMapInv_ι x

Premises used: SymmetricAlgebra.algebraMapInv_ι