H₂ imag axis pos

@[fun_prop]theorem H₂_imag_axis_pos : ResToImagAxis.Pos H₂ := by  constructor  · exact H₂_imag_axis_real  · intro t ht    simp only [Function.resToImagAxis, ResToImagAxis, ht, ↓reduceDIte, H₂]    -- H₂ = Θ₂^4 where Θ₂(it) is real and positive    -- For z with z.im = 0 and z.re > 0, (z^4).re = (z.re)^4 > 0    have hΘ₂_im := Θ₂_imag_axis_real t ht    have hΘ₂_re_pos := Θ₂_imag_axis_re_pos t ht    -- z^4 for z real equals z.re^4    have hpow : (Θ₂ ⟨I * t, by simp [ht]⟩ ^ 4).re =        (Θ₂ ⟨I * t, by simp [ht]⟩).re ^ 4 := by      set z := Θ₂ ⟨I * t, by simp [ht]⟩ with hz_def      have hz_real : z.im = 0 := hΘ₂_im      -- When im = 0, z = z.re (as complex), so z^4 = (z.re)^4      have hz_eq : z = (z.re : ℂ) := by        apply Complex.ext        · simp        · simp [hz_real]      rw [hz_eq]      norm_cast    rw [hpow]    exact pow_pos hΘ₂_re_pos 4