-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : { w : InfinitePlace K // w ≠ w₀ }
h :
  completeFamily K w₀ (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, completeFamily K w₀ w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₁ :
  (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
        else
          (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
            (normAtAllPlaces
              ((mixedEmbedding K : (a : K) → mixedSpace K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w₀ hi))) :
                    𝓞 K)))))
        (↑x : InfinitePlace K) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ)
          (∑ w' : InfinitePlace K,
            (if hi : Eq.{u_1 + 1} (α := InfinitePlace K) w₀ w₀ then fun (w : InfinitePlace K) ↦ (↑w.mult : ℝ)
              else
                (↑(OpenPartialHomeomorph.symm expMap) : realSpace K → realSpace K)
                  (normAtAllPlaces
                    ((mixedEmbedding K : (a : K) → mixedSpace K)
                      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                                  (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w₀) w₀ hi))) :
                          𝓞 K)))))
              w') *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₂ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (∑ w' : InfinitePlace K, (↑w'.mult : ℝ)) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₃ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(∑ x : InfinitePlace K, x.mult) : ℝ) *
        (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₄ :
  (↑(↑x : InfinitePlace K).mult : ℝ) -
      HMul.hMul (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(finrank ℚ K) : ℝ) * (↑(finrank ℚ K) : ℝ)⁻¹ =
    0 x
h₅ : HSub.hSub (α := ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) (↑(↑x : InfinitePlace K).mult : ℝ) = 0 x
h₆ : Eq (α := ℝ) 0 (0 x)
h₇ h₈ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ)
    ((realSpaceToLogSpace : (a : realSpace K) → { w : InfinitePlace K // w ≠ w₀ } → ℝ) (completeFamily K w₀) x) (0 x)

Tactic:
rw [realSpaceToLogSpace_apply, completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq,
    mul_inv_cancel_right₀ (Nat.cast_ne_zero.mpr Module.finrank_pos.ne'), sub_self, Pi.zero_apply]

Premises used: NumberField.InfinitePlace.sum_mult_eq, sub_self, NumberField.mixedEmbedding.fundamentalCone.completeFamily, Pi.zero_apply, dif_pos, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, mul_inv_cancel_right₀, Nat.cast_sum, rfl