by
  let c : Ω → ℝ := actionIndicator A k i
  let g : Ω → 𝓨 := fun ω ↦ Y i ω - env.means A Y (A i ω) i ω
  have h_smul : c • g = {ω | A i ω = k}.indicator (fun ω ↦ Y i ω - env.means A Y (A i ω) i ω) := by
    ext ω
    by_cases hω : A i ω = k <;> simp [c, g, actionIndicator, hω]
  have hAG : Measurable[h.filtrationAction i] (A i) := h.adapted_action_filtrationAction i
  have hcG : StronglyMeasurable[h.filtrationAction i] c :=
    (h.adapted_actionIndicator_filtrationAction k i).stronglyMeasurable
  have hgint : Integrable g P := hint.sub (h.integrable_means_action hint)
  have hcint : Integrable (c • g) P := by
    rw [h_smul]
    exact integrable_noiseSum_increment h hint k
  have hcondg : P[g | h.filtrationAction i] =ᵐ[P] 0 := by
    refine (condExp_sub hint (h.integrable_means_action hint) _).trans ?_
    have h1 := h.condExp_feedback i hint
    grw [h1]
    rw [condExp_of_stronglyMeasurable]
    · simp
    · exact h.adapted_means_filtrationAction.stronglyAdapted i
    · exact h.integrable_means_action hint
  have hpull := condExp_smul_of_aestronglyMeasurable_left hcG.aestronglyMeasurable hcint hgint
  filter_upwards [hpull, hcondg] with ω hp hcg
  rw [← h_smul, hp]
  simp only [Pi.smul_apply', hcg, Pi.ofNat_apply, smul_eq_zero]
  rcases eq_or_ne (A i ω) k with hak | hak
  · simp
  · simp [c, actionIndicator, hak]