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

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp ((lift Q) of)
⊢ C ((s.val.comp ((lift Q) of)) a)

Tactic:
exact Subtype.prop (lift Q of a)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp ((lift Q) of)
⊢ C a

Tactic:
rw [← AlgHom.id_apply (R := R) a, of_id]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp ((lift Q) of)
⊢ C ((s.val.comp ((lift Q) of)) a)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
⊢ C a

Tactic:
letI h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
⊢ C a

Proof state:
case a.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
x✝ : M
⊢ ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ CliffordAlgebra.ι Q) x✝ =
    ((s.val.comp ((lift Q) of)).toLinearMap ∘ₗ CliffordAlgebra.ι Q) x✝

Tactic:
simp [of, h]

Result:
case a.h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := C, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯, algebraMap_mem' := algebraMap }
h : AddCommMonoid ↥s := inferInstanceAs (AddCommMonoid ↥(Subalgebra.toSubmodule s))
of : { f // ∀ (m : M), f m * f m = (_root_.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
x✝ : M
⊢ (CliffordAlgebra.ι Q) x✝ = ↑((LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι) x✝)