R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
⊢ C a
let s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C
    mul_mem' := h_mul _ _
    add_mem' := h_add _ _
    algebraMap_mem' := h_grade0 }
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
⊢ C a
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
let of : X → s := Subtype.coind (ι R) h_grade1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C a
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
⊢ C a
have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) := by
  ext
  simp [Subtype.coind]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C a

case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ a = ↑(↑(↑(lift R) of) a)
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C a
suffices : a = lift R of a
case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : ∀ (x : FreeAlgebra R X), x = ↑(↑(↑(lift R) (Subtype.coind (ι R) h_grade1)) x)
⊢ a = ↑(↑(↑(lift R) of) a)
case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ a = ↑(↑(↑(lift R) of) a)
simp [AlgHom.ext_iff] at of_id
no goals
case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : ∀ (x : FreeAlgebra R X), x = ↑(↑(↑(lift R) (Subtype.coind (ι R) h_grade1)) x)
⊢ a = ↑(↑(↑(lift R) of) a)
exact of_id a
case w.h
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
x✝ : X
⊢ (↑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝ = (↑(AlgHom.comp (Subalgebra.val s) (↑(lift R) of)) ∘ ι R) x✝
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
⊢ AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
ext
no goals
case w.h
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
x✝ : X
⊢ (↑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝ = (↑(AlgHom.comp (Subalgebra.val s) (↑(lift R) of)) ∘ ι R) x✝
simp [Subtype.coind]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C ↑(↑(↑(lift R) of) a)
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C a
rw [this]
no goals
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C ↑(↑(↑(lift R) of) a)
exact Subtype.prop (lift R of a)