F₄ S action

lemma f₄_S_action : (f₄ ∣[(4 : ℤ)] S) = -f₂ := by  -- Step 1: (serre_D 2 H₄)|[4]S = -serre_D 2 H₂ (via equivariance)  have h_serre_term : (serre_D (2 : ℤ) H₄ ∣[(4 : ℤ)] S) = -serre_D (2 : ℤ) H₂ := by    rw [show (4 : ℤ) = 2 + 2 from rfl,        serre_D_slash_equivariant (2 : ℤ) H₄ H₄_SIF_MDifferentiable S, H₄_S_action]    simpa using serre_D_smul 2 (-1) H₂ H₂_SIF_MDifferentiable  -- Step 2: (2•H₂ + H₄)|[2]S = -(2•H₄ + H₂)  have h_lin_comb : (((2 : ℂ) • H₂ + H₄) ∣[(2 : ℤ)] S) = -((2 : ℂ) • H₄ + H₂) := by    rw [add_slash, SL_smul_slash, H₂_S_action, H₄_S_action]    ext z; simp [Pi.add_apply, Pi.smul_apply, Pi.neg_apply]; ring  -- Step 3: Product (H₄ * (2•H₂ + H₄))|[4]S = H₂ * (H₂ + 2•H₄)  have h_prod : ((H₄ * ((2 : ℂ) • H₂ + H₄)) ∣[(4 : ℤ)] S) = H₂ * (H₂ + (2 : ℂ) • H₄) := by    rw [show (4 : ℤ) = 2 + 2 from rfl, mul_slash_SL2 2 2 S _ _, H₄_S_action, h_lin_comb]    ext z; simp [Pi.mul_apply, Pi.neg_apply, Pi.add_apply, Pi.smul_apply]; ring  -- Combine: f₄|[4]S = -serre_D 2 H₂ + (1/6) * H₂ * (H₂ + 2H₄) = -f₂  rw [f₄_decompose, add_slash, SL_smul_slash, h_serre_term, h_prod]  unfold f₂  ext z  simp only [Pi.sub_apply, Pi.add_apply, Pi.smul_apply, Pi.neg_apply, Pi.mul_apply, smul_eq_mul]  ring_nf