-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : { w : InfinitePlace K // w ≠ w₀ }
rw :
  Eq (α := realSpace K)
    ((basisOfLinearIndependentOfCardEqFinrank (b := completeFamily K) ⋯ ⋯ : (a : InfinitePlace K) → realSpace K)
        (↑i : InfinitePlace K) :
      realSpace K)
    ((↑(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))
                      i)) :
                𝓞 K)))) :
      realSpace K)
rw₁ :
  completeFamily K (↑i : InfinitePlace K) =
    (↑(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))
                    i)) :
              𝓞 K))))
rw₂ :
  Eq.{u_1 + 1} (α := realSpace K)
    (if hi : (↑i : InfinitePlace K) = 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₀) (↑i : InfinitePlace K) hi))) :
                𝓞 K)))))
    ((↑(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))
                    i)) :
              𝓞 K)))))
⊢ Eq (α := realSpace K) ((completeBasis K : (a : InfinitePlace K) → realSpace K) (↑i : InfinitePlace K) : realSpace K)
    ((↑(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))
                      i)) :
                𝓞 K)))) :
      realSpace K)
have rw₃ : Eq.{u_1 + 1} (α := realSpace K)
  ((↑(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₀) (↑i : InfinitePlace K) sorry))) :
            𝓞 K)))))
  ((↑(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))
                  i)) :
            𝓞 K)))))
Tactic: rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]