Theta g T action

lemma theta_g_T_action : (theta_g ∣[(6 : ℤ)] T) = theta_g := by  -- Under T: H₂ → -H₂, H₄ → H₃, f₂ → -f₂, f₄ → f₃  -- Linear combination transforms: (2•H₂ + H₄)|T = -2•H₂ + H₃, (H₂ + 2•H₄)|T = -H₂ + 2•H₃  have h_2H₂_H₄ : (((2 : ℂ) • H₂ + H₄) ∣[(2 : ℤ)] T) = -(2 : ℂ) • H₂ + H₃ := by    simp only [add_slash, SL_smul_slash, H₂_T_action, H₄_T_action, smul_neg]    ext z    simp only [Pi.add_apply, Pi.smul_apply, Pi.neg_apply, smul_eq_mul]    ring  have h_H₂_2H₄ : ((H₂ + (2 : ℂ) • H₄) ∣[(2 : ℤ)] T) = -H₂ + (2 : ℂ) • H₃ := by    simp only [add_slash, SL_smul_slash, H₂_T_action, H₄_T_action]  -- Product transforms  have h_term1 : ((((2 : ℂ) • H₂ + H₄) * f₂) ∣[(6 : ℤ)] T) = (-(2 : ℂ) • H₂ + H₃) * (-f₂) := by    have hmul := mul_slash_SL2 2 4 T ((2 : ℂ) • H₂ + H₄) f₂    simp only [h_2H₂_H₄, f₂_T_action] at hmul    exact hmul  have h_term2 : (((H₂ + (2 : ℂ) • H₄) * f₄) ∣[(6 : ℤ)] T) = (-H₂ + (2 : ℂ) • H₃) * f₃ := by    have hmul := mul_slash_SL2 2 4 T (H₂ + (2 : ℂ) • H₄) f₄    simp only [h_H₂_2H₄, f₄_T_action] at hmul    exact hmul  -- Combine and simplify using Jacobi: H₃ = H₂ + H₄, f₃ = f₂ + f₄  simp only [theta_g, add_slash, h_term1, h_term2]  ext z; simp only [Pi.add_apply, Pi.mul_apply, Pi.smul_apply, Pi.neg_apply, smul_eq_mul]  rw [(congrFun jacobi_identity z).symm, (congrFun f₂_add_f₄_eq_f₃ z).symm]  simp only [Pi.add_apply]; ring