-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CMField (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
let let₁ let₂ let₃ let₄ : regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺
let₅ : regOfFamily (realFundSystem K) = |∏ w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }, 2| * regulator.{u_1} ↥K⁺
let₆ :
  let W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀;
  let f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
    Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
      (equivInfinitePlace K) ⋯;
  let g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } :=
    Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm;
  Eq (α := ℝ)
    |Matrix.det (n := { w : InfinitePlace ↥K⁺ // w ≠ w₀ })
        (Matrix.submatrix (m := { w : InfinitePlace K // w ≠ W₀ }) (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)
                        (↑(realFundSystem K ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K)) i)) :
                          𝓞 K) :
                      K)))
            (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ })
            (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) :
          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 j : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
            HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
              ((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 : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
                    (logEmbedding ↥K⁺ : (a : Additive (𝓞 ↥K⁺)ˣ) → logSpace ↥K⁺)
                      ((Additive.ofMul : (a : (𝓞 ↥K⁺)ˣ) → Additive (𝓞 ↥K⁺)ˣ)
                          (fundSystem (↥K⁺)
                            (((Equiv.symm (equivFinRank ↥K⁺) :
                                  { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ≃ Fin (rank.{u_1} ↥K⁺)) :
                                (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → Fin (rank ↥K⁺))
                              i)) :
                        Additive (𝓞 ↥K⁺)ˣ))
                  i j :
                ℝ) :
          Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)|
⊢ regOfFamily (realFundSystem K) = HPow.hPow (α := ℝ) 2 (rank K) * regulator.{u_1} ↥K⁺
have e_a : let W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀;
let f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) sorry;
let g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } :=
  Equiv.trans (Equiv.trans (finCongr sorry) (equivFinRank ↥K⁺)) f.symm;
Eq (α := Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
  (Matrix.submatrix (m := { w : InfinitePlace K // w ≠ W₀ }) (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)
                  (↑(realFundSystem K ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K)) i)) : 𝓞 K) :
                K)))
      (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ })
      (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) :
    Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { 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 j : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
        ((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 : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
              (logEmbedding ↥K⁺ : (a : Additive (𝓞 ↥K⁺)ˣ) → logSpace ↥K⁺)
                ((Additive.ofMul : (a : (𝓞 ↥K⁺)ˣ) → Additive (𝓞 ↥K⁺)ˣ)
                    (fundSystem (↥K⁺)
                      (((Equiv.symm (equivFinRank ↥K⁺) : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ≃ Fin (rank.{u_1} ↥K⁺)) :
                          (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → Fin (rank ↥K⁺))
                        i)) :
                  Additive (𝓞 ↥K⁺)ˣ))
            i j :
          ℝ) :
    Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
Tactic: classical
  let W₀ := (equivInfinitePlace K).symm w₀
  let f : {w : InfinitePlace K // w ≠ W₀} ≃ {w : InfinitePlace K⁺ // w ≠ w₀} :=
    (equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]
  let g := ((finCongr (units_rank_eq_units_rank K).symm).trans (equivFinRank K⁺)).trans f.symm
  rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
  rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det _ W₀ g.symm, regOfFamily_eq_det',
    ← abs_mul, ← Matrix.det_mul_column, ← Matrix.det_reindex_self f, Matrix.reindex_apply]
  congr; ext i w
  rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
  simp [f, g]