-- 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
⊢ Eq (α := ℝ)
    |det.{0, u_1} (n := { 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₀ } ℝ)
          (Function.comp (β :=
            ↥(span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
            (Subtype.val (p := fun (x : { w : InfinitePlace K // w ≠ w₀ } → ℝ) ↦
              Membership.mem (γ := Submodule ℤ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
                (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))) x))
            (Function.comp (β := Fin (rank K))
              (⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) :
                (a : Fin (rank K)) → ↥(span ℤ (Set.range (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
              (⇑(Equiv.symm (equivFinRank K)) : (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K)))))|
    |det (n := { 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)ˣ) :
          Matrix { w : InfinitePlace K // w ≠ w₀ } { w : InfinitePlace K // w ≠ w₀ } ℝ)|
have pos : ∀ (i x : { w : InfinitePlace K // w ≠ w₀ }),
  Eq (α := ℝ)
    (Function.comp (β :=
      ↥(span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
      (Subtype.val (p := fun (x : { w : InfinitePlace K // w ≠ w₀ } → ℝ) ↦
        Membership.mem (γ := Submodule ℤ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ))
          (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))) x))
      (Function.comp (β := Fin (rank K))
        (⇑(Basis.restrictScalars ℤ (basisOfIsMaxRank hu)) :
          (a : Fin (rank K)) → ↥(span ℤ (Set.range (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
        (⇑(Equiv.symm (equivFinRank K)) : (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K)))
      i x)
    ((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)ˣ)
      x)
Tactic: congr 3 with i