Super Commute F grade

lemma superCommuteF_grade {a b : 𝓕.FieldOpFreeAlgebra} {f1 f2 : FieldStatistic}    (ha : a ∈ statisticSubmodule f1) (hb : b ∈ statisticSubmodule f2) :    [a, b]ₛF ∈ statisticSubmodule (f1 + f2) := by  let p (a2 : 𝓕.FieldOpFreeAlgebra) (hx : a2 ∈ statisticSubmodule f2) : Prop :=    [a, a2]ₛF ∈ statisticSubmodule (f1 + f2)  change p b hb  apply Submodule.span_induction (p := p)  · intro x hx    obtain ⟨φs, rfl, hφs⟩ := hx    simp only [add_eq_mul, p]    let p (a2 : 𝓕.FieldOpFreeAlgebra) (hx : a2 ∈ statisticSubmodule f1) : Prop :=        [a2, ofCrAnListF φs]ₛF ∈ statisticSubmodule (f1 + f2)    change p a ha    apply Submodule.span_induction (p := p)    · intro x hx      obtain ⟨φs', rfl, hφs'⟩ := hx      simp only [add_eq_mul, p]      rw [superCommuteF_ofCrAnListF_ofCrAnListF]      apply Submodule.sub_mem _      · apply ofCrAnListF_mem_statisticSubmodule_of        rw [ofList_append_eq_mul, hφs, hφs']      · apply Submodule.smul_mem        apply ofCrAnListF_mem_statisticSubmodule_of        rw [ofList_append_eq_mul, hφs, hφs', mul_comm]    · simp [p]    · intro x y hx hy hp1 hp2      simp only [add_eq_mul, map_add, LinearMap.add_apply, p]      exact Submodule.add_mem _ hp1 hp2    · intro c x hx hp1      simp only [add_eq_mul, map_smul, LinearMap.smul_apply, p]      exact Submodule.smul_mem _ c hp1    · exact ha  · simp [p]  · intro x y hx hy hp1 hp2    simp only [add_eq_mul, map_add, p]    exact Submodule.add_mem _ hp1 hp2  · intro c x hx hp1    simp only [add_eq_mul, map_smul, p]    exact Submodule.smul_mem _ c hp1  · exact hb