-- 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)
simp_rw :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := CliffordAlgebra Q)
      ((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))
      ⊤)
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Subalgebra.map (A := CliffordAlgebra Q)
      ((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))
      (Algebra.adjoin R (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₂ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.image (α := CliffordAlgebra Q)
        (⇑((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)
        (Set.range (ι := M) (⇑(ι Q) : (a : M) → CliffordAlgebra Q))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₃ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.range.{u_3, u_2 + 1} (ι := M)
        (Function.comp (β := CliffordAlgebra Q)
          (⇑((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))))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
simp_rw₄ :
  Eq.{u_3 + 1} (α := Subalgebra R A)
    (Algebra.adjoin R
      (Set.range fun (x : M) ↦
        (((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)))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))
⊢ Eq.{u_3 + 1} (α := Subalgebra R A)
    (AlgHom.range (A := CliffordAlgebra Q)
      ((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)))
    (Algebra.adjoin R (Set.range.{u_3, u_2 + 1} (ι := M) (⇑f : (a : M) → A)))

Tactic:
simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

Premises used: Set.range_comp, CliffordAlgebra.lift_ι_apply, CliffordAlgebra.adjoin_range_ι, AlgHom.map_adjoin, Function.comp_def, Algebra.map_top