-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
have :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₁ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₂ :
  LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    completeFamily K (↑w : InfinitePlace K)
have₃ have₄ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K)),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₅ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K))
    (h₂ :
      completeFamily K w₀ ∉
        Submodule.span ℝ
          (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))),
    LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)
have₆ :
  ∀
    (h₁ :
      LinearIndependent ℝ (M := realSpace K) fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        completeFamily K (↑w : InfinitePlace K))
    (h₂ :
      completeFamily K w₀ ∉
        Submodule.span ℝ
          (Set.range fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦ completeFamily K (↑w : InfinitePlace K))),
    LinearIndependent (ι := { b : InfinitePlace K // b ≠ w₀ }) ℝ (M := realSpace K)
        ((completeFamily K ∘
            (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
          some) ∧
      Function.comp (α := Option { b : InfinitePlace K // b ≠ w₀ }) (completeFamily K)
          (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K) none ∉
        Submodule.span ℝ
          (Set.range (ι := { b : InfinitePlace K // b ≠ w₀ })
            ((completeFamily K ∘
                (⇑(Equiv.optionSubtypeNe w₀) : (a : Option { b : InfinitePlace K // b ≠ w₀ }) → InfinitePlace K)) ∘
              some))
⊢ LinearIndependent (ι := InfinitePlace K) ℝ (completeFamily K)

Tactic:
classical
  have h₁ : LinearIndependent ℝ (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1) := by
    refine LinearIndependent.of_comp realSpaceToLogSpace ?_
    simp_rw [Function.comp_def, realSpaceToLogSpace_completeFamily_of_ne]
    convert! (((basisUnitLattice K).ofZLatticeBasis ℝ _).reindex equivFinRank).linearIndependent
    simp
  have h₂ : completeFamily K w₀ ∉ Submodule.span ℝ
      (Set.range (fun w : {w // w ≠ w₀} ↦ completeFamily K w.1)) := by
    intro h
    have := sum_eq_zero_of_mem_span_completeFamily h
    rw [completeFamily, dif_pos rfl, ← Nat.cast_sum, sum_mult_eq, Nat.cast_eq_zero] at this
    exact Module.finrank_pos.ne' this
  rw [← linearIndependent_equiv (Equiv.optionSubtypeNe w₀), linearIndependent_option]
  exact ⟨h₁, h₂⟩

Premises used: linearIndependent_option, NumberField.Units.dirichletUnitTheorem.w₀, linearIndependent_equiv, Equiv.optionSubtypeNe