-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Regulator (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w : InfinitePlace K // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w : InfinitePlace K // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K :=
  Equiv.trans (finSuccEquiv (rank K))
    (↑((Equiv.symm (Equiv.optionSubtype w₁) :
            (a : Fin (rank K) ≃ { y : InfinitePlace K // y ≠ w₁ }) →
              { e : Option (Fin (rank K)) ≃ InfinitePlace K //
                (e : (a : Option (Fin (rank K))) → InfinitePlace K) none = w₁ })
          e₁.symm) :
      Option (Fin (rank K)) ≃ InfinitePlace K)
g : { w : InfinitePlace K // w ≠ w₂ } ≃ Fin (rank K) :=
  Equiv.trans (β := { b : Fin (rank K + 1) // b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂ })
    (f.symm.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ w₂) (q := fun (b : Fin (rank K + 1)) ↦
      b ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂) ⋯)
    (Equiv.symm (finSuccAboveEquiv ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂)))
h_col :
  Eq (α := ℝ)
    |det (n := { w : InfinitePlace K // w ≠ w₂ })
        (submatrix (m := { 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 : { w : InfinitePlace K // w ≠ w₂ }) ↦
              (↑(↑w : InfinitePlace K).mult : ℝ) *
                Real.log
                  (((↑w : InfinitePlace K) : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(u ((e₂ : (a : { w : InfinitePlace K // w ≠ w₂ }) → Fin (rank K)) i)) : 𝓞 K) :
                      K)))
            (⇑(g.trans e₂.symm) : (a : { w : InfinitePlace K // w ≠ w₂ }) → { w : InfinitePlace K // w ≠ w₂ }) id :
          Matrix { w : InfinitePlace K // w ≠ w₂ } { w : InfinitePlace K // w ≠ w₂ } ℝ)|
    |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 : { w : InfinitePlace K // w ≠ w₂ }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(u ((e₂ : (a : { w : InfinitePlace K // w ≠ w₂ }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w₂ } { w : InfinitePlace K // w ≠ w₂ } ℝ)|
refine_2 :
  ∀
    (h :
      |det (n := Fin (rank K))
            (submatrix
              ((of : (a : Fin (rank K) → Fin (rank K + 1) → ℝ) → Matrix (Fin (rank K)) (Fin (rank K + 1)) ℝ)
                fun (i : Fin (rank K)) (w : Fin (rank K + 1)) ↦
                (↑(mult.{u_1} (K := K) ((f : (a : Fin (rank K + 1)) → InfinitePlace K) w)) : ℝ) *
                  Real.log
                    ((((f : (a : Fin (rank K + 1)) → InfinitePlace K) w : InfinitePlace K) : (a : K) → ℝ)
                      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(u i) : 𝓞 K) : K)))
              id (Fin.succAbove 0))| =
        |HSMul.hSMul (β := ℝ)
            (HSub.hSub (α := ℤ) (↑(↑0 : ℕ) : ℤ)
                (↑(↑((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂) : ℕ) : ℤ)).negOnePow
            (det (n := Fin (rank K))
              (submatrix
                ((of : (a : Fin (rank K) → Fin (rank K + 1) → ℝ) → Matrix (Fin (rank K)) (Fin (rank K + 1)) ℝ)
                  fun (i : Fin (rank K)) (w : Fin (rank K + 1)) ↦
                  (↑(mult.{u_1} (K := K) ((f : (a : Fin (rank K + 1)) → InfinitePlace K) w)) : ℝ) *
                    Real.log
                      ((((f : (a : Fin (rank K + 1)) → InfinitePlace K) w : InfinitePlace K) : (a : K) → ℝ)
                        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(u i) : 𝓞 K) : K)))
                id (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w₂))))|),
    Eq (α := ℝ)
      |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 : { w : InfinitePlace K // w ≠ w₁ }) ↦
              (↑(↑w : InfinitePlace K).mult : ℝ) *
                Real.log
                  (((↑w : InfinitePlace K) : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(u ((e₁ : (a : { w : InfinitePlace K // w ≠ w₁ }) → Fin (rank K)) i)) : 𝓞 K) :
                      K)) :
            Matrix { w : InfinitePlace K // w ≠ w₁ } { w : InfinitePlace K // w ≠ w₁ } ℝ)|
      |det (n := { w : InfinitePlace K // w ≠ w₂ })
          (submatrix (m := { 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 : { w : InfinitePlace K // w ≠ w₂ }) ↦
                (↑(↑w : InfinitePlace K).mult : ℝ) *
                  Real.log
                    (((↑w : InfinitePlace K) : (a : K) → ℝ)
                      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                          (↑(u ((e₂ : (a : { w : InfinitePlace K // w ≠ w₂ }) → Fin (rank K)) i)) : 𝓞 K) :
                        K)))
              (⇑(g.trans e₂.symm) : (a : { w : InfinitePlace K // w ≠ w₂ }) → { w : InfinitePlace K // w ≠ w₂ }) id :
            Matrix { w : InfinitePlace K // w ≠ w₂ } { w : InfinitePlace K // w ≠ w₂ } ℝ)|
⊢ Eq (α := ℝ)
    |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 : { w : InfinitePlace K // w ≠ w₁ }) ↦
            (↑(↑w : InfinitePlace K).mult : ℝ) *
              Real.log
                (((↑w : InfinitePlace K) : (a : K) → ℝ)
                  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                      (↑(u ((e₁ : (a : { w : InfinitePlace K // w ≠ w₁ }) → Fin (rank K)) i)) : 𝓞 K) :
                    K)) :
          Matrix { w : InfinitePlace K // w ≠ w₁ } { w : InfinitePlace K // w ≠ w₁ } ℝ)|
    |det (n := { w : InfinitePlace K // w ≠ w₂ })
        (submatrix (m := { 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 : { w : InfinitePlace K // w ≠ w₂ }) ↦
              (↑(↑w : InfinitePlace K).mult : ℝ) *
                Real.log
                  (((↑w : InfinitePlace K) : (a : K) → ℝ)
                    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                        (↑(u ((e₂ : (a : { w : InfinitePlace K // w ≠ w₂ }) → Fin (rank K)) i)) : 𝓞 K) :
                      K)))
            (⇑(g.trans e₂.symm) : (a : { w : InfinitePlace K // w ≠ w₂ }) → { w : InfinitePlace K // w ≠ w₂ }) id :
          Matrix { w : InfinitePlace K // w ≠ w₂ } { w : InfinitePlace K // w ≠ w₂ } ℝ)|
have refine_1 : ∀ (i : Fin (rank K)),
  Eq (α := ℝ)
    (∑ j : Fin (rank K + 1),
      (of : (a : Fin (rank K) → Fin (rank K + 1) → ℝ) → Matrix (Fin (rank K)) (Fin (rank K + 1)) ℝ)
        (fun (i : Fin (rank K)) (w : Fin (rank K + 1)) ↦
          (↑(mult.{u_1} (K := K) ((f : (a : Fin (rank K + 1)) → InfinitePlace K) w)) : ℝ) *
            Real.log
              ((((f : (a : Fin (rank K + 1)) → InfinitePlace K) w : InfinitePlace K) : (a : K) → ℝ)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(u i) : 𝓞 K) : K)))
        i j)
    0
Tactic: have h := congr_arg abs <| submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det'
    (of fun i w ↦ (mult (f w) : ℝ) * ((f w) (u i)).log) ?_ 0 (f.symm w₂)