-- 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 :
  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₀ } ℝ)|
⊢ regOfFamily u =
    |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:
rw [regOfFamily_of_isMaxRank hu, ZLattice.covolume_eq_det _
      (((basisOfIsMaxRank hu).restrictScalars ℤ).reindex (equivFinRank K)), Basis.coe_reindex]

Premises used: NumberField.Units.equivFinRank, NumberField.Units.regOfFamily_of_isMaxRank, Int, Module.Basis.coe_reindex, NumberField.Units.basisOfIsMaxRank, Module.Basis.restrictScalars, Module.Basis.reindex, ZLattice.covolume_eq_det