-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
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)))
⊢ 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)))
have 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)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]