awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f :
  { f : M →ₗ[R] A //
    ∀ (m : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((↑((fun (F : CliffordAlgebra Q →ₐ[R] A) ↦
                  (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
                      ∀ (m : M),
                        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
                      (F.toLinearMap ∘ₗ ι Q) ⋯ :
                    { f : M →ₗ[R] A //
                      ∀ (m : M),
                        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }))
                ((fun
                      (f :
                        { f : M →ₗ[R] A //
                          ∀ (m : M),
                            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }) ↦
                    ((RingQuot.liftAlgHom R (s := Rel Q) :
                          (a :
                              { f : TensorAlgebra R M →ₐ[R] A //
                                ∀ ⦃x y : TensorAlgebra R M⦄,
                                  Rel Q x y →
                                    (f : (a : TensorAlgebra R M) → A) x = (f : (a : TensorAlgebra R M) → A) y }) →
                            RingQuot (Rel Q) →ₐ[R] A)
                        (Subtype.mk (p := fun (f : TensorAlgebra R M →ₐ[R] A) ↦
                          ∀ ⦃x y : TensorAlgebra R M⦄,
                            Rel Q x y →
                              Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A)
                                ((f : (a : TensorAlgebra R M) → A) y : A))
                          ((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A)) ⋯) :
                      RingQuot (Rel Q) →ₐ[R] A))
                  f)) :
            M →ₗ[R] A) :
          (a : M) → A)
        x :
      A)
    (((↑f : M →ₗ[R] A) : (a : M) → A) x : A)

Tactic:
(RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)

Premises used: TensorAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f :
  { f : M →ₗ[R] A //
    ∀ (m : M),
      HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
        (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }
x : M
⊢ Eq.{u_3 + 1} (α := A)
    (((↑((fun (F : CliffordAlgebra Q →ₐ[R] A) ↦
                  (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
                      ∀ (m : M),
                        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
                      (F.toLinearMap ∘ₗ ι Q) ⋯ :
                    { f : M →ₗ[R] A //
                      ∀ (m : M),
                        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }))
                ((fun
                      (f :
                        { f : M →ₗ[R] A //
                          ∀ (m : M),
                            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }) ↦
                    ((RingQuot.liftAlgHom R (s := Rel Q) :
                          (a :
                              { f : TensorAlgebra R M →ₐ[R] A //
                                ∀ ⦃x y : TensorAlgebra R M⦄,
                                  Rel Q x y →
                                    (f : (a : TensorAlgebra R M) → A) x = (f : (a : TensorAlgebra R M) → A) y }) →
                            RingQuot (Rel Q) →ₐ[R] A)
                        (Subtype.mk (p := fun (f : TensorAlgebra R M →ₐ[R] A) ↦
                          ∀ ⦃x y : TensorAlgebra R M⦄,
                            Rel Q x y →
                              Eq.{u_3 + 1} (α := A) ((f : (a : TensorAlgebra R M) → A) x : A)
                                ((f : (a : TensorAlgebra R M) → A) y : A))
                          ((TensorAlgebra.lift R : (a : M →ₗ[R] A) → TensorAlgebra R M →ₐ[R] A) (↑f : M →ₗ[R] A)) ⋯) :
                      RingQuot (Rel Q) →ₐ[R] A))
                  f)) :
            M →ₗ[R] A) :
          (a : M) → A)
        x :
      A)
    (((↑f : M →ₗ[R] A) : (a : M) → A) x : A)

Tactic:
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)

Premises used: TensorAlgebra.lift_ι_apply, RingQuot.liftAlgHom_mkAlgHom_apply, Eq.trans
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
⊢ AlgHom.toLinearMap
        ((lift Q :
            (a :
                { f : M →ₗ[R] A //
                  ∀ (m : M),
                    (f : (a : M) → A) m * (f : (a : M) → A) m =
                      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
              CliffordAlgebra Q →ₐ[R] A)
          (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
            ∀ (m : M),
              HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
            f cond)) ∘ₗ
      ι Q =
    f

Tactic:
Subtype.mk_eq_mk.mp <| (lift Q).symm_apply_apply ⟨f, cond⟩

Premises used: Equiv.symm_apply_apply, Subtype.mk, CliffordAlgebra.lift, Subtype.mk_eq_mk, Iff.mp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
x : M
⊢ Eq.{u_3 + 1} (α := A)
    ((((lift Q :
                (a :
                    { f : M →ₗ[R] A //
                      ∀ (m : M),
                        (f : (a : M) → A) m * (f : (a : M) → A) m =
                          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
                  CliffordAlgebra Q →ₐ[R] A)
              (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
                ∀ (m : M),
                  HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
                    (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
                f cond) :
            CliffordAlgebra Q →ₐ[R] A) :
          (a : CliffordAlgebra Q) → A)
        ((ι Q : (a : M) → CliffordAlgebra Q) x : CliffordAlgebra Q) :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
(LinearMap.ext_iff.mp <| ι_comp_lift f cond) x

Premises used: CliffordAlgebra.ι_comp_lift, LinearMap.ext_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
g : CliffordAlgebra Q →ₐ[R] A
⊢ Eq (α :=
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      ((Equiv.symm (lift Q) :
            (a : CliffordAlgebra Q →ₐ[R] A) →
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) })
          g :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) }) ↔
    g =
      (lift Q :
          (a :
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] A)
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond)

Tactic:
(lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq

Premises used: Equiv.symm_apply_eq, CliffordAlgebra.lift
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
g : CliffordAlgebra Q →ₐ[R] A
h :
  g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      ((Equiv.symm (lift Q) :
            (a : CliffordAlgebra Q →ₐ[R] A) →
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) })
          g :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
⊢ g.toLinearMap ∘ₗ ι Q = f ↔
    g =
      (lift Q :
          (a :
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] A)
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond)

Tactic:
convert! (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq

Premises used: Equiv.symm_apply_eq, CliffordAlgebra.lift
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond :
  ∀ (m : M),
    HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
      (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R)
g : CliffordAlgebra Q →ₐ[R] A
h :
  g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
        (g.toLinearMap ∘ₗ ι Q) ⋯)
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
        f cond)
h₁ h₂ : g.toLinearMap ∘ₗ ι Q = f ↔ g.toLinearMap ∘ₗ ι Q = f
⊢ g.toLinearMap ∘ₗ ι Q = f ↔
    Eq (α :=
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      ((Equiv.symm (lift Q) :
            (a : CliffordAlgebra Q →ₐ[R] A) →
              { f : M →ₗ[R] A //
                ∀ (m : M),
                  (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) })
          g :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
          f cond :
        { f : M →ₗ[R] A //
          ∀ (m : M),
            HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
              (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })

Tactic:
rw [lift_symm_apply, Subtype.mk_eq_mk]

Premises used: CliffordAlgebra.lift_symm_apply, Subtype.mk_eq_mk
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q :
        (a :
            { f : M →ₗ[R] A //
              ∀ (m : M),
                (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
          CliffordAlgebra Q →ₐ[R] A)
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
        (g.toLinearMap ∘ₗ ι Q) ⋯) =
    g

Tactic:
(lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, CliffordAlgebra.lift
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
g : CliffordAlgebra Q →ₐ[R] A
⊢ (lift Q :
        (a :
            { f : M →ₗ[R] A //
              ∀ (m : M),
                (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) }) →
          CliffordAlgebra Q →ₐ[R] A)
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
        (g.toLinearMap ∘ₗ ι Q) ⋯) =
    g

Tactic:
exact (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, CliffordAlgebra.lift
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_4
inst_3 : Semiring A
inst_4 : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
a :
  Eq (α :=
    { f : M →ₗ[R] A //
      ∀ (m : M),
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
    ((Equiv.symm (lift Q) :
          (a : CliffordAlgebra Q →ₐ[R] A) →
            { f : M →ₗ[R] A //
              ∀ (m : M),
                (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) })
        f :
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
    ((Equiv.symm (lift Q) :
          (a : CliffordAlgebra Q →ₐ[R] A) →
            { f : M →ₗ[R] A //
              ∀ (m : M),
                (f : (a : M) → A) m * (f : (a : M) → A) m = (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m) })
        g :
      { f : M →ₗ[R] A //
        ∀ (m : M),
          HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
            (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
⊢ f = g

Tactic:
apply (lift Q).symm.injective

Premises used: CliffordAlgebra.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_4
inst_3 : Semiring A
inst_4 : Algebra R A
f g : CliffordAlgebra Q →ₐ[R] A
h : f.toLinearMap ∘ₗ ι Q = g.toLinearMap ∘ₗ ι Q
⊢ Eq (α :=
    { f : M →ₗ[R] A //
      ∀ (m : M),
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R) })
    (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
      ∀ (m : M),
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
      (f.toLinearMap ∘ₗ ι Q) ⋯)
    (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
      ∀ (m : M),
        HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) =
          (algebraMap R A : (a : R) → A) ((Q : (a : M) → R) m : R))
      (g.toLinearMap ∘ₗ ι Q) ⋯)

Tactic:
simp only [h]
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q : (a : M) → 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
let : C a
⊢ C a

Tactic:
let s : Subalgebra R (CliffordAlgebra Q) :=
    { carrier := C
      mul_mem' := @mul
      add_mem' := @add
      algebraMap_mem' := algebraMap }
-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q : (a : M) → 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 }
of : { f : M →ₗ[R] ↥s //
  ∀ (m : M),
    HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
      (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) } :=
  Subtype.mk (p := fun (f : M →ₗ[R] ↥s) ↦
    ∀ (m : M),
      HMul.hMul (α := ↥s) (β := ↥s) ((f : (a : M) → ↥s) m : ↥s) ((f : (a : M) → ↥s) m : ↥s) =
        (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m))
    (LinearMap.codRestrict
      ((Subalgebra.toSubmodule : (a : Subalgebra R (CliffordAlgebra Q)) → Submodule R (CliffordAlgebra Q)) s)
      (CliffordAlgebra.ι Q) ι)
    ⋯
a₁ :
  ∀ (x : M),
    Eq (α := CliffordAlgebra Q)
      ((AlgHom.toLinearMap
                (s.val.comp
                  ((lift Q :
                      (a :
                          { f : M →ₗ[R] ↥s //
                            ∀ (m : M),
                              (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                                (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
                        CliffordAlgebra Q →ₐ[R] ↥s)
                    of)) ∘ₗ
              CliffordAlgebra.ι Q :
            (a : M) → CliffordAlgebra Q)
          x :
        CliffordAlgebra Q)
      ((AlgHom.toLinearMap (AlgHom.id R (CliffordAlgebra Q)) ∘ₗ CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) x :
        CliffordAlgebra Q)
⊢ s.val.comp
      ((lift Q :
          (a :
              { f : M →ₗ[R] ↥s //
                ∀ (m : M),
                  (f : (a : M) → ↥s) m * (f : (a : M) → ↥s) m =
                    (Algebra.algebraMap R ↥s : (a : R) → ↥s) ((Q : (a : M) → R) m) }) →
            CliffordAlgebra Q →ₐ[R] ↥s)
        of) =
    AlgHom.id R (CliffordAlgebra Q)

Tactic:
ext x