have h₁ : (2 : Int) ^ 2 = 4 := by norm_num
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z