-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w' : InfinitePlace K
e : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
rw :
  regOfFamily (fundSystem K) =
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
rw₁ :
  Eq (α := ℝ)
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
w'₁ : InfinitePlace K
e₁ : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
rw₂ :
  Eq (α := ℝ)
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|
w'₂ : InfinitePlace K
e₂ : { w : InfinitePlace K // w ≠ w' } ≃ Fin (rank K)
⊢ regulator K =
    |Matrix.det (n := { w : InfinitePlace K // w ≠ w' })
        ((Matrix.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 : { w : InfinitePlace K // w ≠ w' }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ)|

Tactic:
rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det]

Premises used: NumberField.Units.regOfFamily_eq_det, NumberField.Units.regulator_eq_regOfFamily_fundSystem