-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
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)))))
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) ⋯))) :
              𝓞 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)))))
hnc : ¬(↑i : InfinitePlace K) = w₀
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) ⋯))) :
              𝓞 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)))))
hnc₁ : ¬(↑i : InfinitePlace K) = w₀
⊢ 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)

Tactic:
rw [completeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, completeFamily, dif_neg]

Premises used: NumberField.mixedEmbedding.fundamentalCone.completeFamily, coe_basisOfLinearIndependentOfCardEqFinrank, dif_neg, NumberField.mixedEmbedding.fundamentalCone.completeBasis