[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑(ι Q) m * ↑(ι Q) m = ↑(algebraMap R (CliffordAlgebra Q)) (↑Q m)
[PROOFSTEP]
erw [← AlgHom.map_mul, RingQuot.mkAlgHom_rel R (Rel.of m), AlgHom.commutes]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑(algebraMap R (RingQuot (Rel Q))) (↑Q m) = ↑(algebraMap R (CliffordAlgebra Q)) (↑Q m)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ ↑g (↑(ι Q) m) * ↑g (↑(ι Q) m) = ↑(algebraMap R A) (↑Q m)
[PROOFSTEP]
rw [← AlgHom.map_mul, ι_sq_scalar, AlgHom.commutes]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x y : TensorAlgebra R M
h : Rel Q x y
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y
[PROOFSTEP]
induction h
[GOAL]
case of
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x y : TensorAlgebra R M
m✝ : M
⊢ ↑(↑(TensorAlgebra.lift R) ↑f) (↑(TensorAlgebra.ι R) m✝ * ↑(TensorAlgebra.ι R) m✝) =
    ↑(↑(TensorAlgebra.lift R) ↑f) (↑(algebraMap R (TensorAlgebra R M)) (↑Q m✝))
[PROOFSTEP]
rw [AlgHom.commutes, AlgHom.map_mul, TensorAlgebra.lift_ι_apply, f.prop]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
    ↑(algebraMap R A) (↑Q m)
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
⊢ (fun F =>
        { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
          property :=
            (_ :
              ∀ (m : M),
                ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                  ↑(algebraMap R A) (↑Q m)) })
      ((fun f =>
          ↑(RingQuot.liftAlgHom R)
            { val := ↑(TensorAlgebra.lift R) ↑f,
              property :=
                (_ :
                  ∀ (x y : TensorAlgebra R M),
                    Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
ext x
[GOAL]
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
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m) }
x : M
⊢ ↑↑((fun F =>
              { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
                property :=
                  (_ :
                    ∀ (m : M),
                      ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m *
                          ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                        ↑(algebraMap R A) (↑Q m)) })
            ((fun f =>
                ↑(RingQuot.liftAlgHom R)
                  { val := ↑(TensorAlgebra.lift R) ↑f,
                    property :=
                      (_ :
                        ∀ (x y : TensorAlgebra R M),
                          Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
              f))
      x =
    ↑↑f x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
x : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp
              ((fun f =>
                  ↑(RingQuot.liftAlgHom R)
                    { val := ↑(TensorAlgebra.lift R) ↑f,
                      property :=
                        (_ :
                          ∀ (x y : TensorAlgebra R M),
                            Rel Q x y → ↑(↑(TensorAlgebra.lift R) ↑f) x = ↑(↑(TensorAlgebra.lift R) ↑f) y) })
                ((fun F =>
                    { val := LinearMap.comp (AlgHom.toLinearMap F) (ι Q),
                      property :=
                        (_ :
                          ∀ (m : M),
                            ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m *
                                ↑(LinearMap.comp (AlgHom.toLinearMap F) (ι Q)) m =
                              ↑(algebraMap R A) (↑Q m)) })
                  F))
              (RingQuot.mkAlgHom R fun x y => Rel Q x y)))
          (TensorAlgebra.ι R))
      x =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp F (RingQuot.mkAlgHom R fun x y => Rel Q x y)))
          (TensorAlgebra.ι R))
      x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ _)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι Q) = f ↔ g = ↑(lift Q) { val := f, property := cond }
[PROOFSTEP]
convert (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq
[GOAL]
case h.e'_1.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι Q) = f ↔ ↑(lift Q).symm g = { val := f, property := cond }
[PROOFSTEP]
rw [lift_symm_apply, Subtype.mk_eq_mk]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ ↑(lift Q)
      { val := LinearMap.comp (AlgHom.toLinearMap g) (ι Q),
        property := (_ : ∀ (m : M), ↑g (↑(ι Q) m) * ↑g (↑(ι Q) m) = ↑(algebraMap R A) (↑Q m)) } =
    g
[PROOFSTEP]
exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q) → f = g
[PROOFSTEP]
intro h
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ f = g
[PROOFSTEP]
apply (lift Q).symm.injective
[GOAL]
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ ↑(lift Q).symm f = ↑(lift Q).symm g
[PROOFSTEP]
rw [lift_symm_apply, lift_symm_apply]
[GOAL]
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A✝ : Type u_3
inst✝³ : Semiring A✝
inst✝² : Algebra R A✝
A : Type u_4
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : LinearMap.comp (AlgHom.toLinearMap f) (ι Q) = LinearMap.comp (AlgHom.toLinearMap g) (ι Q)
⊢ { val := LinearMap.comp (AlgHom.toLinearMap f) (ι Q),
      property :=
        (_ :
          ∀ (m : M),
            ↑(LinearMap.comp (AlgHom.toLinearMap f) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap f) (ι Q)) m =
              ↑(algebraMap R A) (↑Q m)) } =
    { val := LinearMap.comp (AlgHom.toLinearMap g) (ι Q),
      property :=
        (_ :
          ∀ (m : M),
            ↑(LinearMap.comp (AlgHom.toLinearMap g) (ι Q)) m * ↑(LinearMap.comp (AlgHom.toLinearMap g) (ι Q)) m =
              ↑(algebraMap R A) (↑Q m)) }
[PROOFSTEP]
simp only [h]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
⊢ C a
[PROOFSTEP]
let s : Subalgebra R (CliffordAlgebra Q) :=
  { 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✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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]
letI h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f : M →ₗ[R] s // ∀ m, f m * f m = algebraMap _ _ (Q m) } :=
  ⟨(ι Q).codRestrict (Subalgebra.toSubmodule s) h_grade1, fun m => Subtype.eq <| ι_sq_scalar Q m⟩
    -- the mapping through the subalgebra is the identity
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
⊢ C a
[PROOFSTEP]
have of_id : AlgHom.id R (CliffordAlgebra Q) = s.val.comp (lift Q of) :=
  by
  ext
  simp
    -- porting note: `simp` can't apply this
  erw [LinearMap.codRestrict_apply]
    -- finding a proof is finding an element of the subalgebra
      -- porting note: was `convert Subtype.prop (lift Q of a); exact AlgHom.congr_fun of_id a`
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
⊢ AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
[PROOFSTEP]
ext
[GOAL]
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
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q))) (ι Q)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (Subalgebra.val s) (↑(lift Q) of))) (ι Q)) x✝
[PROOFSTEP]
simp
  -- porting note: `simp` can't apply this
[GOAL]
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
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
x✝ : M
⊢ ↑(ι Q) x✝ = ↑(↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) x✝)
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
  -- finding a proof is finding an element of the subalgebra
    -- porting note: was `convert Subtype.prop (lift Q of a); exact AlgHom.congr_fun of_id a`
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
of_id : AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
⊢ C a
[PROOFSTEP]
rw [← AlgHom.id_apply (R := R) a, of_id]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
C : CliffordAlgebra Q → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (CliffordAlgebra Q)) r)
h_grade1 : ∀ (x : M), C (↑(ι Q) x)
h_mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
h_add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  {
    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 : { f // ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R { x // x ∈ s }) (↑Q m) } :=
  { val := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1,
    property :=
      (_ :
        ∀ (m : M),
          ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m *
              ↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι Q) h_grade1) m =
            ↑(algebraMap R { x // x ∈ s }) (↑Q m)) }
of_id : AlgHom.id R (CliffordAlgebra Q) = AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)
⊢ C (↑(AlgHom.comp (Subalgebra.val s) (↑(lift Q) of)) a)
[PROOFSTEP]
exact Subtype.prop (lift Q of a)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) (a + b) * ↑(ι Q) (a + b) - ↑(ι Q) a * ↑(ι Q) a - ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
rw [(ι Q).map_add, mul_add, add_mul, add_mul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) a * ↑(ι Q) a + ↑(ι Q) b * ↑(ι Q) a + (↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) b) - ↑(ι Q) a * ↑(ι Q) a -
      ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) a =
    ↑(ι Q) a * ↑(ι Q) a + ↑(ι Q) b * ↑(ι Q) a + (↑(ι Q) a * ↑(ι Q) b + ↑(ι Q) b * ↑(ι Q) b) - ↑(ι Q) a * ↑(ι Q) a -
      ↑(ι Q) b * ↑(ι Q) b
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) (a + b) * ↑(ι Q) (a + b) - ↑(ι Q) a * ↑(ι Q) a - ↑(ι Q) b * ↑(ι Q) b =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b)) - ↑(algebraMap R (CliffordAlgebra Q)) (↑Q a) -
      ↑(algebraMap R (CliffordAlgebra Q)) (↑Q b)
[PROOFSTEP]
rw [ι_sq_scalar, ι_sq_scalar, ι_sq_scalar]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b)) - ↑(algebraMap R (CliffordAlgebra Q)) (↑Q a) -
      ↑(algebraMap R (CliffordAlgebra Q)) (↑Q b) =
    ↑(algebraMap R (CliffordAlgebra Q)) (↑Q (a + b) - ↑Q a - ↑Q b)
[PROOFSTEP]
rw [← RingHom.map_sub, ← RingHom.map_sub]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : M
⊢ ↑(ι Q) a * ↑(ι Q) b * ↑(ι Q) a = ↑(ι Q) (QuadraticForm.polar (↑Q) a b • a - ↑Q a • b)
[PROOFSTEP]
rw [ι_mul_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ← Algebra.smul_def, ← map_smul,
  ← map_smul, ← map_sub]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), ↑f m * ↑f m = ↑(algebraMap R A) (↑Q m)
⊢ Submodule.map (AlgHom.toLinearMap (↑(lift Q) { val := f, property := cond })) (LinearMap.range (ι Q)) =
    LinearMap.range f
[PROOFSTEP]
rw [← LinearMap.range_comp, ι_comp_lift]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ map Q₁ Q₁ LinearMap.id (_ : ∀ (m : M₁), ↑Q₁ (↑LinearMap.id m) = ↑Q₁ (↑LinearMap.id m)) =
    AlgHom.id R (CliffordAlgebra Q₁)
[PROOFSTEP]
ext m
[GOAL]
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
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
m : M₁
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap (map Q₁ Q₁ LinearMap.id (_ : ∀ (m : M₁), ↑Q₁ (↑LinearMap.id m) = ↑Q₁ (↑LinearMap.id m))))
          (ι Q₁))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q₁))) (ι Q₁)) m
[PROOFSTEP]
exact map_apply_ι _ _ _ _ m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
⊢ AlgHom.comp (map Q₂ Q₃ f hf) (map Q₁ Q₂ g hg) =
    map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)
[PROOFSTEP]
ext m
[GOAL]
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
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
m : M₁
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (map Q₂ Q₃ f hf) (map Q₁ Q₂ g hg))) (ι Q₁)) m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)))
          (ι Q₁))
      m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]
[GOAL]
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
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : M₂ →ₗ[R] M₃
hf : ∀ (m : M₂), ↑Q₃ (↑f m) = ↑Q₂ m
g : M₁ →ₗ[R] M₂
hg : ∀ (m : M₁), ↑Q₂ (↑g m) = ↑Q₁ m
m : M₁
⊢ ↑(map Q₂ Q₃ f hf) (↑(map Q₁ Q₂ g hg) (↑(ι Q₁) m)) =
    ↑(map Q₁ Q₃ (LinearMap.comp f g) (_ : ∀ (m : M₁), ↑Q₃ (↑f (↑g m)) = ↑Q₁ m)) (↑(ι Q₁) m)
[PROOFSTEP]
rw [map_apply_ι, map_apply_ι, map_apply_ι, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ map Q₂ Q₂ (LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e))
      (_ : ∀ (m : M₂), ↑Q₂ (↑↑↑e (↑↑↑(QuadraticForm.IsometryEquiv.symm e) m)) = ↑Q₂ m) =
    AlgHom.id R (CliffordAlgebra Q₂)
[PROOFSTEP]
convert map_id Q₂ using 2
  -- porting note: replaced `_` with `Q₂`
[GOAL]
case h.e'_2.h.e'_11
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e) = LinearMap.id
[PROOFSTEP]
ext m
[GOAL]
case h.e'_2.h.e'_11.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
m : M₂
⊢ ↑(LinearMap.comp ↑↑e ↑↑(QuadraticForm.IsometryEquiv.symm e)) m = ↑LinearMap.id m
[PROOFSTEP]
exact e.toLinearEquiv.apply_symm_apply m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ map Q₁ Q₁ (LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e)
      (_ : ∀ (m : M₁), ↑Q₁ (↑↑↑(QuadraticForm.IsometryEquiv.symm e) (↑↑↑e m)) = ↑Q₁ m) =
    AlgHom.id R (CliffordAlgebra Q₁)
[PROOFSTEP]
convert map_id Q₁ using 2
  -- porting note: replaced `_` with `Q₁`
[GOAL]
case h.e'_2.h.e'_11
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
⊢ LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e = LinearMap.id
[PROOFSTEP]
ext m
[GOAL]
case h.e'_2.h.e'_11.h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e : QuadraticForm.IsometryEquiv Q₁ Q₂
m : M₁
⊢ ↑(LinearMap.comp ↑↑(QuadraticForm.IsometryEquiv.symm e) ↑↑e) m = ↑LinearMap.id m
[PROOFSTEP]
exact e.toLinearEquiv.symm_apply_apply m
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticForm.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticForm.IsometryEquiv Q₂ Q₃
⊢ AlgEquiv.trans (equivOfIsometry e₁₂) (equivOfIsometry e₂₃) =
    equivOfIsometry (QuadraticForm.IsometryEquiv.trans e₁₂ e₂₃)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
e₁₂ : QuadraticForm.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticForm.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ ↑(AlgEquiv.trans (equivOfIsometry e₁₂) (equivOfIsometry e₂₃)) x =
    ↑(equivOfIsometry (QuadraticForm.IsometryEquiv.trans e₁₂ e₂₃)) x
[PROOFSTEP]
exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x
[GOAL]
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
⊢ equivOfIsometry (QuadraticForm.IsometryEquiv.refl Q₁) = AlgEquiv.refl
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
x : CliffordAlgebra Q₁
⊢ ↑(equivOfIsometry (QuadraticForm.IsometryEquiv.refl Q₁)) x = ↑AlgEquiv.refl x
[PROOFSTEP]
exact AlgHom.congr_fun (map_id Q₁) x
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
m : M
inst✝ : Invertible (↑Q m)
⊢ ↑(ι Q) (⅟(↑Q m) • m) * ↑(ι Q) m = 1
[PROOFSTEP]
rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
m : M
inst✝ : Invertible (↑Q m)
⊢ ↑(ι Q) m * ↑(ι Q) (⅟(↑Q m) • m) = 1
[PROOFSTEP]
rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
m : M
inst✝¹ : Invertible (↑Q m)
inst✝ : Invertible (↑(ι Q) m)
⊢ ⅟(↑(ι Q) m) = ↑(ι Q) (⅟(↑Q m) • m)
[PROOFSTEP]
letI := invertibleιOfInvertible Q m
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
m : M
inst✝¹ : Invertible (↑Q m)
inst✝ : Invertible (↑(ι Q) m)
this : Invertible (↑(ι Q) m) := invertibleιOfInvertible Q m
⊢ ⅟(↑(ι Q) m) = ↑(ι Q) (⅟(↑Q m) • m)
[PROOFSTEP]
convert (rfl : ⅟(ι Q m) = _)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
val✝ : Invertible (↑Q m)
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
letI := invertibleιOfInvertible Q m
[GOAL]
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
h : IsUnit (↑Q m)
val✝ : Invertible (↑Q m)
this : Invertible (↑(ι Q) m) := invertibleιOfInvertible Q m
⊢ IsUnit (↑(ι Q) m)
[PROOFSTEP]
exact isUnit_of_invertible (ι Q m)
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
a b : M
inst✝¹ : Invertible (↑(ι Q) a)
inst✝ : Invertible (↑Q a)
⊢ ↑(ι Q) a * ↑(ι Q) b * ⅟(↑(ι Q) a) = ↑(ι Q) ((⅟(↑Q a) * QuadraticForm.polar (↑Q) a b) • a - b)
[PROOFSTEP]
rw [invOf_ι, map_smul, mul_smul_comm, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul, invOf_mul_self,
  one_smul]
[GOAL]
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
n : ℕ
A : Type u_3
inst✝³ : Semiring A
inst✝² : Algebra R A
a b : M
inst✝¹ : Invertible (↑(ι Q) a)
inst✝ : Invertible (↑Q a)
⊢ ⅟(↑(ι Q) a) * ↑(ι Q) b * ↑(ι Q) a = ↑(ι Q) ((⅟(↑Q a) * QuadraticForm.polar (↑Q) a b) • a - b)
[PROOFSTEP]
rw [invOf_ι, map_smul, smul_mul_assoc, smul_mul_assoc, ι_mul_ι_mul_ι, ← map_smul, smul_sub, smul_smul, smul_smul,
  invOf_mul_self, one_smul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ℕ
m : M
⊢ ↑toClifford (↑(ι R) m) = ↑(CliffordAlgebra.ι Q) m
[PROOFSTEP]
simp [toClifford]
