diff --git a/nevanlinna/logabs.lean b/nevanlinna/logabs.lean
index e5b5d9d..dc92c6d 100644
--- a/nevanlinna/logabs.lean
+++ b/nevanlinna/logabs.lean
@@ -46,7 +46,7 @@ lemma logAbsXX : ∀ z : ℂ, z ≠ 0 → Real.log (Complex.abs z) = (1 / 2) * C
   rw [t₃]
   rw [Complex.normSq_eq_conj_mul_self]
   
-  have : conj z ≠ 0 := by
+  have t₄ : conj z ≠ 0 := by
     exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr z₁Hyp
 
   let XX := Complex.log_mul_eq_add_log_iff this z₁Hyp