-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
inst_3 : Ring A
inst_4 : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
m₁ : M
snd :
  ∀ (x : M →ₗ[R] A)
    (h :
      Membership.mem (γ := Set (M →ₗ[R] A))
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)}
        x),
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A)
snd₁ :
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((0 : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((0 : (a : M) → A) m₁ : A)
snd₂ :
  ∀ (x y : M →ₗ[R] A)
    (hx :
      Membership.mem (γ := Submodule R (M →ₗ[R] A))
        (Submodule.span R
          {f' : M →ₗ[R] A |
            ∃ (x : A) (m₂ : M),
              f' =
                (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                  (LinearMap.mulRight R x)})
        x)
    (hy :
      Membership.mem (γ := Submodule R (M →ₗ[R] A))
        (Submodule.span R
          {f' : M →ₗ[R] A |
            ∃ (x : A) (m₂ : M),
              f' =
                (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                  (LinearMap.mulRight R x)})
        y),
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
          ((x : (a : M) → A) m : A) =
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A) →
      HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
            ((y : (a : M) → A) m : A) =
          HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((y : (a : M) → A) m₁ : A) →
        HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
            ((x + y : (a : M) → A) m : A) =
          HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x + y : (a : M) → A) m₁ : A)
⊢ HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
      ((g : (a : M) → A) m : A) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((g : (a : M) → A) m₁ : A)
have snd₃ : ∀ (a : R) (x : M →ₗ[R] A)
  (hx :
    Membership.mem (γ := Submodule R (M →ₗ[R] A))
      (Submodule.span R
        {f' : M →ₗ[R] A |
          ∃ (x : A) (m₂ : M),
            f' =
              (LinearMap.lcomp R A ((f.bilin.flip : (a : M) → M →ₗ[R] A) m₂) : (a : A →ₗ[R] A) → M →ₗ[R] A)
                (LinearMap.mulRight R x)})
      x),
  HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((x : (a : M) → A) m₁ : A) →
    HMul.hMul (α := A) (β := A) ((((f.bilin : (a : M) → M →ₗ[R] A) m₁ : M →ₗ[R] A) : (a : M) → A) m : A)
        ((a • x : (a : M) → A) m : A) =
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := A) ((Q : (a : M) → R) m : R) ((a • x : (a : M) → A) m₁ : A)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hg