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
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
let s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := C
    mul_mem' := @h_mul
    add_mem' := @h_add
    algebraMap_mem' := h_grade0 }
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
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
let h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
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
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
let of : M →ₗ[R] s := (ι R).codRestrict (Subalgebra.toSubmodule s) h_grade1
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
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
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
  ext
  simp
  erw [LinearMap.codRestrict_apply]
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)
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
rw [← AlgHom.id_apply (R := R) a, of_id]
no goals
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)
exact Subtype.prop (lift R of a)
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✝
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)
ext
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✝)
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✝
simp
no goals
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✝)
erw [LinearMap.codRestrict_apply]