diff --git a/Mathlib/Analysis/Complex/CanonicalDecomposition.lean b/Mathlib/Analysis/Complex/CanonicalDecomposition.lean
index c12b3682f64313..315e96018ec4d0 100644
--- a/Mathlib/Analysis/Complex/CanonicalDecomposition.lean
+++ b/Mathlib/Analysis/Complex/CanonicalDecomposition.lean
@@ -72,7 +72,7 @@ variable (R w) in
 /--
 Canonical factors are meromorphic.
 -/
-theorem meromorphic_canonicalFactor : Meromorphic (canonicalFactor R w) := by
+@[fun_prop] theorem meromorphic_canonicalFactor : Meromorphic (canonicalFactor R w) := by
   intro x
   unfold canonicalFactor
   fun_prop
@@ -513,4 +513,127 @@ theorem _root_.MeromorphicOn.exists_ecanonicalDecomp (h₁f : MeromorphicOn f (c
       simp_all [← smul_assoc]
     }
 
+/--
+Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
+decomposition, write the function `h` entirely in terms of `f`.
+-/
+lemma ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAt
+    {f h : ℂ → E} (D : ECanonicalDecomp f h R) (hw : w ∈ closedBall 0 R) (hR : 0 < R) :
+    h w
+      = ((∏ᶠ i, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f (ball 0 R) i))
+          * (∏ᶠ i, meromorphicTrailingCoeffAt (· - i) w ^ (-divisor f (sphere 0 R)) i))
+          • meromorphicTrailingCoeffAt f w := by
+  -- Finiteness properties and side results used throughout the proof
+  have h₃f : (divisor f (sphere 0 R)).support.Finite := divisor_sphere_support_finite
+  have h₄f : (divisor f (ball 0 R)).support.Finite := D.meromorphicOn.divisor_ball_support_finite
+  have := (D.analyticOnNhd w hw).meromorphicAt
+  -- Proof body: Substitute `f` using `h₁f` and compute
+  rw [meromorphicTrailingCoeffAt_congr_nhdsNE
+    ((D.meromorphicOn w hw).eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin_preperfect
+      (by fun_prop) hw _ D.eventuallyEq),
+    finprod_eq_prod_of_mulSupport_subset (s := h₄f.toFinset) _ (by aesop),
+    finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _ (by aesop),
+    finprod_eq_prod_of_mulSupport_subset (s := h₄f.toFinset) _ (by aesop),
+    finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _ (by aesop),
+    MeromorphicAt.meromorphicTrailingCoeffAt_smul (by fun_prop)
+      (D.analyticOnNhd w hw).meromorphicAt,
+    MeromorphicAt.meromorphicTrailingCoeffAt_mul (by fun_prop) (by fun_prop),
+    meromorphicTrailingCoeffAt_prod (by fun_prop), meromorphicTrailingCoeffAt_prod (by fun_prop),
+    (D.analyticOnNhd w hw).meromorphicTrailingCoeffAt_of_ne_zero (D.ne_zero w hw), smul_smul,
+    mul_mul_mul_comm,
+    ← Finset.prod_mul_distrib, ← Finset.prod_mul_distrib, Finset.prod_eq_one, Finset.prod_eq_one,
+    mul_one, one_smul]
+  · intro x hx
+    rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀,
+      locallyFinsuppWithin.coe_neg, Pi.neg_apply, neg_add_cancel, zpow_zero]
+    rw [meromorphicTrailingCoeffAt_id_sub_const]
+    grind
+  · intro x hx
+    rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop), ← zpow_add₀, add_neg_cancel,
+      zpow_zero]
+    apply MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero (by fun_prop)
+      (meromorphicOrderAt_canonicalFactor_ne_top x hR)
+  · rw [← closure_ball _ hR.ne']
+    exact isOpen_ball.perfect_closure.2
+
+/--
+Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
+decomposition, write the function `h` entirely in terms of `f`, under the assumption that `f` has
+order zero.
+-/
+lemma ECanonicalDecomp.eq_smul_meromorphicTrailingCoeffAt_of_meromorphicOrderAt
+    {f h : ℂ → E} (D : ECanonicalDecomp f h R) (h₁w : w ∈ closedBall 0 R)
+    (h₂w : meromorphicOrderAt f w = 0) (hR : 0 < R) :
+    h w = ((∏ᶠ i, (canonicalFactor R i w) ^ (divisor f (ball 0 R) i))
+          * (∏ᶠ i, (w - i) ^ (-divisor f (sphere 0 R)) i))
+          • meromorphicTrailingCoeffAt f w := by
+  rw [D.eq_smul_meromorphicTrailingCoeffAt h₁w hR]
+  congr
+  · ext x
+    by_cases h₃x : (divisor f (ball 0 R)) x = 0
+    · simp [h₃x]
+    have h₁x : x ∈ ball 0 R := (divisor f (ball 0 R)).supportWithinDomain h₃x
+    have h₂x : w ≠ x := by
+      rintro rfl
+      exact h₃x (by simp [(D.meromorphicOn.mono_set ball_subset_closedBall).divisor_apply h₁x, h₂w])
+    rw [AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero
+      (Complex.analyticOnNhd_canonicalFactor R x w h₂x)
+      (Complex.canonicalFactor_ne_zero h₁x h₁w h₂x)]
+  · ext x
+    by_cases h : x = w
+    · simp_all [meromorphicTrailingCoeffAt_id_sub_const, divisor_def]
+    grind [meromorphicTrailingCoeffAt_id_sub_const]
+
+/--
+Companion lemma to `MeromorphicOn.exists_ecanonicalDecomp`: In the setting of the extended canonical
+decomposition, write the function `log ‖h‖` entirely in terms of `f`, under the assumption that `f`
+has order zero.
+-/
+lemma ECanonicalDecomp.log_norm_eq
+    {f h : ℂ → E} (D : ECanonicalDecomp f h R) (h₁w : w ∈ closedBall 0 R)
+    (h₂w : meromorphicOrderAt f w = 0)
+    (hR : 0 < R) :
+    Real.log ‖h w‖ = ((∑ᶠ i, (divisor f (ball 0 R) i) * Real.log ‖canonicalFactor R i w‖)
+          - (∑ᶠ i, (divisor f (sphere 0 R) i) * Real.log ‖w - i‖))
+          + Real.log ‖meromorphicTrailingCoeffAt f w‖ := by
+  have h₃f : (divisor f (sphere 0 R)).support.Finite := divisor_sphere_support_finite
+  have h₄f : (divisor f (ball 0 R)).support.Finite := D.meromorphicOn.divisor_ball_support_finite
+  have η₀ : ∀ x ∈ h₃f.toFinset, ‖w - x‖ ^ (-divisor f (sphere 0 R)) x ≠ 0 := by
+    intro x hx
+    rw [Finite.mem_toFinset] at hx
+    refine zpow_ne_zero _ ?_
+    rw [norm_ne_zero_iff, sub_ne_zero]
+    rintro rfl
+    exact hx (by simp [divisor_apply (D.meromorphicOn.mono_set sphere_subset_closedBall)
+      ((divisor f (sphere 0 R)).supportWithinDomain hx), h₂w])
+  have η₁ : ∀ x ∈ h₄f.toFinset, ‖canonicalFactor R x w‖ ^ (divisor f (ball 0 R)) x ≠ 0 := by
+    intro x hx
+    rw [Finite.mem_toFinset] at hx
+    refine zpow_ne_zero _ ?_
+    rw [ne_eq, norm_eq_zero]
+    have h₁x : x ∈ ball 0 R := (divisor f (ball 0 R)).supportWithinDomain hx
+    refine canonicalFactor_ne_zero h₁x h₁w ?_
+    rintro rfl
+    exact hx (by simp [divisor_apply (D.meromorphicOn.mono_set ball_subset_closedBall) h₁x, h₂w])
+  rw [D.eq_smul_meromorphicTrailingCoeffAt_of_meromorphicOrderAt
+    h₁w h₂w hR, finprod_eq_prod_of_mulSupport_subset (s := h₄f.toFinset) _ (by aesop),
+    finprod_eq_prod_of_mulSupport_subset (s := h₃f.toFinset) _ (by aesop),
+    finsum_eq_sum_of_support_subset (s := h₄f.toFinset) _ (fun _ _ ↦ (by aesop)),
+    finsum_eq_sum_of_support_subset (s := h₃f.toFinset) _ (fun _ _ ↦ (by aesop)), norm_smul,
+    norm_mul, norm_prod, norm_prod]
+  simp_rw [norm_zpow]
+  rw [Real.log_mul (mul_ne_zero_iff.2 ⟨Finset.prod_ne_zero_iff.2 η₁, Finset.prod_ne_zero_iff.2 η₀⟩),
+    Real.log_mul (Finset.prod_ne_zero_iff.2 η₁) (Finset.prod_ne_zero_iff.2 η₀), Real.log_prod η₁,
+    Real.log_prod η₀]
+  · congr
+    · ext i
+      exact log_zpow ‖canonicalFactor R i w‖ ((divisor f (ball 0 R)) i)
+    · rw [← Finset.sum_neg_distrib]
+      apply Finset.sum_congr rfl
+      intro i hi
+      rw [log_zpow ‖w - i‖ ((-divisor f (sphere 0 R)) i)]
+      simp
+  · rw [ne_eq, norm_eq_zero]
+    apply (D.meromorphicOn w h₁w).meromorphicTrailingCoeffAt_ne_zero (by aesop)
+
 end Complex