diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
index 8461636..d67a0d3 100644
--- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
+++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean
@@ -51,16 +51,16 @@ lemma int₀
 
   -- case: a ≠ 0
   simp_rw [l₂]
-  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
+  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
   conv =>
     left
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_neg ((fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
+  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
 
-  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := by
+  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
+  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
     dsimp [f₁]
     congr 4
     let A := periodic_circleMap 0 1 x
@@ -71,7 +71,7 @@ lemma int₀
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
   simp
   dsimp [f₁]
 
@@ -82,7 +82,7 @@ lemma int₀
     · exact norm_pos_iff'.mpr h₁a
     · exact mem_ball_zero_iff.mp ha
 
-  let F := fun z ↦ Real.log ‖1 - z * a‖
+  let F := fun z ↦ log ‖1 - z * a‖
 
   have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
     intro x hx
@@ -105,7 +105,7 @@ lemma int₀
     rw [← h] at this
     simp at this
 
-  let A := harmonic_meanValue ρ 1 Real.zero_lt_one hρ hf
+  let A := harmonic_meanValue ρ 1 zero_lt_one hρ hf
   dsimp [F] at A
   simp at A
   exact A
@@ -163,7 +163,7 @@ lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (
   _ = 2 - 2 * cos (2 * (x / 2)) := by
     rw [← mul_div_assoc]
     congr; norm_num
-  _ = 4 - 4 * Real.cos (x / 2) ^ 2 := by
+  _ = 4 - 4 * cos (x / 2) ^ 2 := by
     rw [cos_two_mul]
     ring
   _ = 4 * sin (x / 2) ^ 2 := by
@@ -172,12 +172,20 @@ lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (
 
 lemma int'₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖
   IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume 0 (2 * π) := by
+
   simp_rw [logAffineHelper]
+  apply IntervalIntegrable.div_const
   rw [← IntervalIntegrable.comp_mul_left_iff (c := 2) (Ne.symm (NeZero.ne' 2))]
   simp
 
-  sorry
-
+  have h₁ : Set.EqOn (fun x => log (4 * sin x ^ 2)) (fun x => log 4 + 2 * log (sin x)) (Set.Ioo 0 π) := by
+    intro x hx
+    simp [log_mul (Ne.symm (NeZero.ne' 4)), log_pow, ne_of_gt (sin_pos_of_mem_Ioo hx)]
+  rw [IntervalIntegrable.integral_congr_Ioo pi_nonneg h₁]
+  apply IntervalIntegrable.add
+  simp
+  apply IntervalIntegrable.const_mul
+  exact intervalIntegrable_log_sin
 
 lemma int₁ :
   ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
@@ -208,19 +216,19 @@ lemma int₁ :
 lemma int₂
   {a : ℂ}
   (ha : ‖a‖ = 1) :
-  ∫ x in (0)..(2 * Real.pi), log ‖circleMap 0 1 x - a‖ = 0 := by
+  ∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
 
   simp_rw [l₂]
-  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
+  have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
   conv =>
     left
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_neg ((fun w ↦ Real.log ‖1 - circleMap 0 1 (w) * a‖))]
+  rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
 
-  let f₁ := fun w ↦ Real.log ‖1 - circleMap 0 1 w * a‖
-  have {x : ℝ} : Real.log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * Real.pi) := by
+  let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
+  have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
     dsimp [f₁]
     congr 4
     let A := periodic_circleMap 0 1 x
@@ -231,7 +239,7 @@ lemma int₂
     arg 1
     intro x
     rw [this]
-  rw [intervalIntegral.integral_comp_add_right f₁ (2 * Real.pi)]
+  rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
   simp
   dsimp [f₁]