-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem induction {C : TensorAlgebra R M → Prop}
    (algebraMap : ∀ r, C (algebraMap R (TensorAlgebra R M) r)) (ι : ∀ x, C (ι R x))
    (mul : ∀ a b, C a → C b → C (a * b)) (add : ∀ a b, C a → C b → C (a + b))
    (a : TensorAlgebra R M) : C a

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) 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 := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
⊢ C a

Tactic:
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
  ext
  simp only [AlgHom.toLinearMap_id, LinearMap.id_comp, AlgHom.comp_toLinearMap,
    LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, lift_ι_apply,
    Subalgebra.coe_val]
  erw [LinearMap.codRestrict_apply]

Result:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) 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 := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)
⊢ C a

Proof state:
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
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) 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 := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
x✝ : M
⊢ (TensorAlgebra.ι R) x✝ = ↑(of x✝)

Tactic:
erw [LinearMap.codRestrict_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) 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 := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
⊢ AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)

Tactic:
ext

Result:
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
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) 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 := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
x✝ : M
⊢ ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝ =
    ((s.val.comp ((lift R) of)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝