From 98efcf9f872cd90822286f5f27b054eca26a32fc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 25 Apr 2024 19:16:21 +0200
Subject: [PATCH] Update logabs.lean

---
 nevanlinna/logabs.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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