-- 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)))
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)))
⊢ 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.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)))
Tactic: simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]