-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
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)
⊢ 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₀ } ℝ)|

Tactic:
congr 3 with i