[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y
[PROOFSTEP]
rw [← AlgHom.map_add]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
    ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R x + FreeAlgebra.ι R y)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel R Rel.add
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : M
⊢ AddHom.toFun
      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
        map_add' :=
          (_ :
            ∀ (x y : M),
              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
          map_add' :=
            (_ :
              ∀ (x y : M),
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
        x
[PROOFSTEP]
rw [← AlgHom.map_smul]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : M
⊢ AddHom.toFun
      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
        map_add' :=
          (_ :
            ∀ (x y : M),
              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
      (r • x) =
    ↑(RingQuot.mkAlgHom R (Rel R M)) (↑(RingHom.id R) r • FreeAlgebra.ι R x)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel R Rel.smul
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = ↑(ι R) m
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    ↑{
          toAddHom :=
            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M),
                AddHom.toFun
                    { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                      map_add' :=
                        (_ :
                          ∀ (x y : M),
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      x) }
      m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
h : Rel R M x y
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y
[PROOFSTEP]
induction h
[GOAL]
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
a✝ b✝ : M
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R (a✝ + b✝)) =
    ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R a✝ + FreeAlgebra.ι R b✝)
[PROOFSTEP]
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, map_mul, AlgHom.commutes,
  map_add]
[GOAL]
case smul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
r✝ : R
a✝ : M
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R (r✝ • a✝)) =
    ↑(↑(FreeAlgebra.lift R) ↑f) (↑(algebraMap R (FreeAlgebra R M)) r✝ * FreeAlgebra.ι R a✝)
[PROOFSTEP]
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, map_mul, AlgHom.commutes,
  map_add]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F => LinearMap.comp (AlgHom.toLinearMap F) (ι R))
      ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
          { val := ↑(FreeAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ (x y : FreeAlgebra R M),
                  Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F =>
        LinearMap.comp (AlgHom.toLinearMap F)
          {
            toAddHom :=
              { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                map_add' :=
                  (_ :
                    ∀ (x y : M),
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M),
                  AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      (r • x) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                          map_add' :=
                            (_ :
                              ∀ (x y : M),
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                        x) })
      ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
          { val := ↑(FreeAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ (x y : FreeAlgebra R M),
                  Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
ext1 x
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ↑((fun F =>
            LinearMap.comp (AlgHom.toLinearMap F)
              {
                toAddHom :=
                  { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                    map_add' :=
                      (_ :
                        ∀ (x y : M),
                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M),
                      AddHom.toFun
                          { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                            map_add' :=
                              (_ :
                                ∀ (x y : M),
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                          (r • x) =
                        ↑(RingHom.id R) r •
                          AddHom.toFun
                            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                              map_add' :=
                                (_ :
                                  ∀ (x y : M),
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                            x) })
          ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
              { val := ↑(FreeAlgebra.lift R) ↑f,
                property :=
                  (_ :
                    ∀ (x y : FreeAlgebra R M),
                      Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
            f))
      x =
    ↑f x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (↑(AlgHom.comp
            ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
                { val := ↑(FreeAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ (x y : FreeAlgebra R M),
                        Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
              ((fun F => LinearMap.comp (AlgHom.toLinearMap F) (ι R)) F))
            (RingQuot.mkAlgHom R (Rel R M))) ∘
        FreeAlgebra.ι R)
      x =
    (↑(AlgHom.comp F (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (↑(AlgHom.comp
            ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
                { val := ↑(FreeAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ (x y : FreeAlgebra R M),
                        Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
              ((fun F =>
                  LinearMap.comp (AlgHom.toLinearMap F)
                    {
                      toAddHom :=
                        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                          map_add' :=
                            (_ :
                              ∀ (x y : M),
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : M),
                            AddHom.toFun
                                { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : M),
                                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                                (r • x) =
                              ↑(RingHom.id R) r •
                                AddHom.toFun
                                  { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : M),
                                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                                  x) })
                F))
            (RingQuot.mkAlgHom R (Rel R M))) ∘
        FreeAlgebra.ι R)
      x =
    (↑(AlgHom.comp F (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply _ _)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap (↑(lift R) f)) (ι R) = f
[PROOFSTEP]
convert (lift R).symm_apply_apply f
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ↑(↑(lift R) f) (↑(ι R) x) = ↑f x
[PROOFSTEP]
conv_rhs => rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ g = ↑(lift R) f
[PROOFSTEP]
rw [← (lift R).symm_apply_eq]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ ↑(lift R).symm g = f
[PROOFSTEP]
simp only [lift, Equiv.coe_fn_symm_mk]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (LinearMap.comp (AlgHom.toLinearMap g) (ι R)) = g
[PROOFSTEP]
rw [← lift_symm_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (↑(lift R).symm g) = g
[PROOFSTEP]
exact (lift R).apply_symm_apply g
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : LinearMap.comp (AlgHom.toLinearMap f) (ι R) = LinearMap.comp (AlgHom.toLinearMap g) (ι R)
⊢ f = g
[PROOFSTEP]
rw [← lift_symm_apply, ← lift_symm_apply] at w 
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
[PROOFSTEP]
exact (lift R).symm.injective w
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
⊢ C a
[PROOFSTEP]
let s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := C
    mul_mem' := @h_mul
    add_mem' := @h_add
    algebraMap_mem' := h_grade0 }
    -- porting note: Added `h`. `h` is needed for `of`.
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
[PROOFSTEP]
let h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
⊢ C a
[PROOFSTEP]
let of : M →ₗ[R] s := (ι R).codRestrict (Subalgebra.toSubmodule s) h_grade1
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
⊢ C a
[PROOFSTEP]
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) :=
  by
  ext
  simp
  erw [LinearMap.codRestrict_apply]
    -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
⊢ AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M))) (ι R)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (Subalgebra.val s) (↑(lift R) of))) (ι R)) x✝
[PROOFSTEP]
simp
[GOAL]
case w.h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
x✝ : M
⊢ ↑(ι R) x✝ = ↑(↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1) x✝)
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
  -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
of_id : AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C a
[PROOFSTEP]
rw [← AlgHom.id_apply (R := R) a, of_id]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
of_id : AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C (↑(AlgHom.comp (Subalgebra.val s) (↑(lift R) of)) a)
[PROOFSTEP]
exact Subtype.prop (lift R of a)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (TensorAlgebra R M)) x) = x
[PROOFSTEP]
simp [algebraMapInv]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ↑ιInv (↑(ι R) x) = x
[PROOFSTEP]
simp [ιInv, (AlgHom.toLinearMap_apply), toTrivSqZeroExt_ι _]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ↑(ι R) x = 0 ↔ x = 0
[PROOFSTEP]
rw [← ι_inj R x 0, LinearMap.map_zero]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
rw [h, AlgHom.commutes] at hf0 
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
exact this.symm.imp_left Eq.symm
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(ι R) 0 = ↑(algebraMap R (TensorAlgebra R M)) 0
[PROOFSTEP]
rw [LinearMap.map_zero, RingHom.map_zero]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ↑(ι R) x ≠ 1
[PROOFSTEP]
rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne.def, ι_eq_algebraMap_iff]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)
[PROOFSTEP]
exact one_ne_zero ∘ And.right
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Disjoint (LinearMap.range (ι R)) 1
[PROOFSTEP]
rw [Submodule.disjoint_def]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x : TensorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
[PROOFSTEP]
rintro _ ⟨x, hx⟩ ⟨r, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : ↑(ι R) x = ↑(Algebra.linearMap R (TensorAlgebra R M)) r
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
[PROOFSTEP]
rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx 
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
[PROOFSTEP]
rw [hx.2, map_zero]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑toTensor (ι R m) = ↑(TensorAlgebra.ι R) m
[PROOFSTEP]
simp [toTensor]
