awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := A)
      (((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
                (F.toLinearMap ∘ₗ
                    {
                      toFun := fun (m : M) ↦
                        (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
                          (FreeAlgebra.ι R m),
                      map_add' := ⋯, map_smul' := ⋯ } :
                  M →ₗ[R] A))
              (Function.comp (β :=
                { f : FreeAlgebra R M →ₐ[R] A //
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A) })
                (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                  (a :
                      { f : FreeAlgebra R M →ₐ[R] A //
                        ∀ ⦃x y : FreeAlgebra R M⦄,
                          Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                    RingQuot (Rel R M) →ₐ[R] A)
                (fun (f : M →ₗ[R] A) ↦
                  Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                    ∀ ⦃x y : FreeAlgebra R M⦄,
                      Rel R M x y →
                        Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                          ((f : (a : FreeAlgebra R M) → A) y : A))
                    ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
                f) :
            (a : M) → A)
          x :
        A)
      ((f : (a : M) → A) x : A)
⊢ (fun (F : TensorAlgebra R M →ₐ[R] A) ↦
        (F.toLinearMap ∘ₗ
            {
              toFun := fun (m : M) ↦
                (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
              map_add' := ⋯, map_smul' := ⋯ } :
          M →ₗ[R] A))
      (Function.comp (β :=
        { f : FreeAlgebra R M →ₐ[R] A //
          ∀ ⦃x y : FreeAlgebra R M⦄,
            Rel R M x y →
              Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A) })
        (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
          (a :
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
            RingQuot (Rel R M) →ₐ[R] A)
        (fun (f : M →ₗ[R] A) ↦
          Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
            ∀ ⦃x y : FreeAlgebra R M⦄,
              Rel R M x y →
                Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A) ((f : (a : FreeAlgebra R M) → A) y : A))
            ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
        f) =
    f

Tactic:
ext1 x
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
              (F.toLinearMap ∘ₗ
                  {
                    toFun := fun (m : M) ↦
                      (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
                    map_add' := ⋯, map_smul' := ⋯ } :
                M →ₗ[R] A))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
(RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)

Premises used: FreeAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
              (F.toLinearMap ∘ₗ
                  {
                    toFun := fun (m : M) ↦
                      (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M)) (FreeAlgebra.ι R m),
                    map_add' := ⋯, map_smul' := ⋯ } :
                M →ₗ[R] A))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              f) :
          (a : M) → A)
        x :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)

Premises used: FreeAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, DFunLike.coe, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (Function.comp (β := FreeAlgebra R M)
      (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
                  (F.toLinearMap ∘ₗ
                      {
                        toFun := fun (m : M) ↦
                          (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
                            (FreeAlgebra.ι R m),
                        map_add' := ⋯, map_smul' := ⋯ } :
                    M →ₗ[R] A))
                F))
            (RingQuot.mkAlgHom R (Rel R M))) :
        (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)

Tactic:
(RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply _ _)

Premises used: FreeAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (Function.comp (β := FreeAlgebra R M)
      (⇑(AlgHom.comp (B := RingQuot (R := FreeAlgebra R M) (Rel R M))
            (Function.comp (β :=
              { f : FreeAlgebra R M →ₐ[R] A //
                ∀ ⦃x y : FreeAlgebra R M⦄,
                  Rel R M x y →
                    Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                      ((f : (a : FreeAlgebra R M) → A) y : A) })
              (⇑(RingQuot.liftAlgHom R (s := Rel R M)) :
                (a :
                    { f : FreeAlgebra R M →ₐ[R] A //
                      ∀ ⦃x y : FreeAlgebra R M⦄,
                        Rel R M x y → (f : (a : FreeAlgebra R M) → A) x = (f : (a : FreeAlgebra R M) → A) y }) →
                  RingQuot (Rel R M) →ₐ[R] A)
              (fun (f : M →ₗ[R] A) ↦
                Subtype.mk (p := fun (f : FreeAlgebra R M →ₐ[R] A) ↦
                  ∀ ⦃x y : FreeAlgebra R M⦄,
                    Rel R M x y →
                      Eq.{u_3 + 1} (α := A) ((f : (a : FreeAlgebra R M) → A) x : A)
                        ((f : (a : FreeAlgebra R M) → A) y : A))
                  ((FreeAlgebra.lift R : (a : M → A) → FreeAlgebra R M →ₐ[R] A) (⇑f : (a : M) → A)) ⋯)
              ((fun (F : TensorAlgebra R M →ₐ[R] A) ↦
                  (F.toLinearMap ∘ₗ
                      {
                        toFun := fun (m : M) ↦
                          (RingQuot.mkAlgHom R (Rel R M) : (a : FreeAlgebra R M) → RingQuot (Rel R M))
                            (FreeAlgebra.ι R m),
                        map_add' := ⋯, map_smul' := ⋯ } :
                    M →ₗ[R] A))
                F))
            (RingQuot.mkAlgHom R (Rel R M))) :
        (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R M) (⇑(F.comp (RingQuot.mkAlgHom R (Rel R M))) : (a : FreeAlgebra R M) → A)
      (FreeAlgebra.ι R) x)

Tactic:
exact
              (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply _ _)

Premises used: FreeAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, Eq.trans
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ (Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A)
      ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) =
    f

Tactic:
(lift R).symm_apply_apply f

Premises used: Equiv.symm_apply_apply, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
⊢ AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R = f

Tactic:
convert! (lift R).symm_apply_apply f

Premises used: Equiv.symm_apply_apply, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
rw : ((AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R : (a : M) → A) x : A)
| ((f : (a : M) → A) x : A)

Tactic:
rw [← ι_comp_lift f]

Premises used: TensorAlgebra.ι_comp_lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
conv_rhs :
  Eq.{u_3 + 1} (α := A)
    ((((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) :
      A)
    ((AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R : (a : M) → A) x : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
conv_rhs => rw [← ι_comp_lift f]

Premises used: TensorAlgebra.ι_comp_lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
x : M
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f : TensorAlgebra R M →ₐ[R] A) :
          (a : TensorAlgebra R M) → A)
        ((ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M) :
      A)
    ((AlgHom.toLinearMap ((lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f) ∘ₗ ι R : (a : M) → A) x : A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
rw : g.toLinearMap ∘ₗ ι R = f ↔ (Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g = f
⊢ g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) f

Tactic:
rw [← (lift R).symm_apply_eq]

Premises used: Equiv.symm_apply_eq, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ (Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g = f

Tactic:
simp only [lift, Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
rw :
  (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A)
      ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g) =
    g
⊢ (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (g.toLinearMap ∘ₗ ι R) = g

Tactic:
rw [← lift_symm_apply]

Premises used: TensorAlgebra.lift_symm_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A)
      ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g) =
    g

Tactic:
(lift R).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ (lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A)
      ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g) =
    g

Tactic:
exact (lift R).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, TensorAlgebra.lift
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ Eq (α := M →ₗ[R] A) ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) f : M →ₗ[R] A)
    ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g : M →ₗ[R] A)

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w

Premises used: TensorAlgebra.lift_symm_apply
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w :
  Eq (α := M →ₗ[R] A) ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) f : M →ₗ[R] A)
    ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g : M →ₗ[R] A)
⊢ f = g

Tactic:
(lift R).symm.injective w

Premises used: TensorAlgebra.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w :
  Eq (α := M →ₗ[R] A) ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) f : M →ₗ[R] A)
    ((Equiv.symm (lift R) : (a : TensorAlgebra R M →ₐ[R] A) → M →ₗ[R] A) g : M →ₗ[R] A)
⊢ f = g

Tactic:
exact (lift R).symm.injective w

Premises used: TensorAlgebra.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
let : C a
⊢ C a

Tactic:
let s : Subalgebra R (TensorAlgebra R M) :=
    { carrier := {a | C a}
      mul_mem' := @mul
      add_mem' := @add
      algebraMap_mem' := algebraMap }
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
x : M
⊢ Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
    ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
⊢ ∀ {x : M},
    Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)

Tactic:
have of_apply {x : M} : of x = (TensorAlgebra.ι R) x := by rfl
-- Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M) : (a : R) → TensorAlgebra R M) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a : TensorAlgebra R M | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s :=
  LinearMap.codRestrict
    ((Subalgebra.toSubmodule : (a : Subalgebra R (TensorAlgebra R M)) → Submodule R (TensorAlgebra R M)) s)
    (TensorAlgebra.ι R) ι
of_apply :
  ∀ {x : M},
    Eq (α := TensorAlgebra R M) ((↑((of : (a : M) → ↥s) x) : TensorAlgebra R M) : TensorAlgebra R M)
      ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x : TensorAlgebra R M)
w :
  ∀ (x : M),
    Eq (α := TensorAlgebra R M)
      ((AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M)) ∘ₗ TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x :
        TensorAlgebra R M)
      ((AlgHom.toLinearMap (s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)) ∘ₗ
              TensorAlgebra.ι R :
            (a : M) → TensorAlgebra R M)
          x :
        TensorAlgebra R M)
⊢ AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R : (a : M →ₗ[R] ↥s) → TensorAlgebra R M →ₐ[R] ↥s) of)

Tactic:
ext