-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
neg :
  ∀
    (hu :
      ¬LinearIndependent.{0, 0, u_1} ℝ (M := logSpace K) fun (i : Fin (rank K)) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)),
    ¬LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
        (of :
            (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) →
              Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)
          (fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
                  (u
                    (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                        (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                      i)) :
                Additive (𝓞 K)ˣ))
          i
⊢ ¬LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (of :
          (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) →
            Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)
        (fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
                (u
                  (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    i)) :
              Additive (𝓞 K)ˣ))
        i
have neg₁ : ∀
  (hu :
    ¬LinearIndependent (ι := { w : InfinitePlace K // w ≠ w₀ }) ℝ (M := logSpace K)
        ((fun (i : Fin (rank K)) ↦
            (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ)) ∘
          (⇑(Equiv.symm (equivFinRank K)) : (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K)))),
  ¬LinearIndependent ℝ (M := { w : InfinitePlace K // w ≠ w₀ } → ℝ) fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (of :
          (a : { w : InfinitePlace K // w ≠ w₀ } → { w : InfinitePlace K // w ≠ w₀ } → ℝ) →
            Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)
        (fun (i : { w : InfinitePlace K // w ≠ w₀ }) ↦
          (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
                (u
                  (((Equiv.symm (equivFinRank K) : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                      (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                    i)) :
              Additive (𝓞 K)ˣ))
        i
Tactic: rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu
Cleared hypotheses: hu