-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
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 :
  (↑(finrank ℚ K) : ℝ) * regOfFamily (fundSystem K) =
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w' then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
⊢ (↑(finrank ℚ K) : ℝ) * regulator K =
    |Matrix.det (n := InfinitePlace K)
        ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
            fun (i w : InfinitePlace K) ↦
            if h : i = w' then (↑w.mult : ℝ)
            else
              (↑w.mult : ℝ) *
                Real.log
                  ((w : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(fundSystem K
                              ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                          𝓞 K) :
                      K)) :
          Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
have rw₁ : Eq (α := ℝ)
  |Matrix.det (n := InfinitePlace K)
      ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          fun (i w : InfinitePlace K) ↦
          if h : i = w' then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                        𝓞 K) :
                    K)) :
        Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
  |Matrix.det (n := InfinitePlace K)
      ((Matrix.of : (a : InfinitePlace K → InfinitePlace K → ℝ) → Matrix (InfinitePlace K) (InfinitePlace K) ℝ)
          fun (i w : InfinitePlace K) ↦
          if h : i = w' then (↑w.mult : ℝ)
          else
            (↑w.mult : ℝ) *
              Real.log
                ((w : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(fundSystem K
                            ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                              (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                        𝓞 K) :
                    K)) :
        Matrix (InfinitePlace K) (InfinitePlace K) ℝ)|
Tactic: rw [regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det]