theorem eta_logDeriv_eql (z : UpperHalfPlane) : logDeriv (ModularForm.eta ∘ fun (z : ℂ) => -1 / z) ↑z = logDeriv (csqrt * ModularForm.eta) ↑z

theorem eta_logderivs : Set.EqOn (logDeriv (ModularForm.eta ∘ fun (z : ℂ) => -1 / z)) (logDeriv (csqrt * ModularForm.eta)) {z : ℂ | 0 < z.im}

theorem eta_logderivs_const : ∃ (z : ℂ), z ≠ 0 ∧ Set.EqOn (ModularForm.eta ∘ fun (z : ℂ) => -1 / z) (z • (csqrt * ModularForm.eta)) {z : ℂ | 0 < z.im}

theorem eta_equality : Set.EqOn (ModularForm.eta ∘ fun (z : ℂ) => -1 / z) ((csqrt Complex.I)⁻¹ • (csqrt * ModularForm.eta)) {z : ℂ | 0 < z.im}