-- 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' : InfinitePlace 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')))
rw :
  (↑(finrank ℚ K) : ℝ) * regOfFamily u =
    HMul.hMul (α := ℝ)
      |∑ j : Fin (rank K + 1),
          ((reindex f.symm f.symm :
                Matrix (InfinitePlace K) (InfinitePlace K) ℝ ≃ Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ) :
              (a : Matrix (InfinitePlace K) (InfinitePlace K) ℝ) → Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ)
            ((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)
                          (↑(u
                                ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                  (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                            𝓞 K) :
                        K)))
            ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') j|
      |det (n := Fin (rank K))
          (submatrix
            (((reindex f.symm f.symm :
                  Matrix (InfinitePlace K) (InfinitePlace K) ℝ ≃ Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ) :
                (a : Matrix (InfinitePlace K) (InfinitePlace K) ℝ) → Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ)
              ((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)
                            (↑(u
                                  ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                    (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                              𝓞 K) :
                          K))))
            (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w'))
            (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w')))|
⊢ (↑(finrank ℚ K) : ℝ) * regOfFamily u =
    |det (n := InfinitePlace K)
        ((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)
                        (↑(u
                              ((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₁ : ∀ (i : Fin (rank K + 1)),
  i ≠ (f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w' →
    Eq (α := ℝ)
      (∑ j : Fin (rank K + 1),
        ((reindex f.symm f.symm :
              Matrix (InfinitePlace K) (InfinitePlace K) ℝ ≃ Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ) :
            (a : Matrix (InfinitePlace K) (InfinitePlace K) ℝ) → Matrix (Fin (rank K + 1)) (Fin (rank K + 1)) ℝ)
          ((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)
                        (↑(u
                              ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                                (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w ≠ w') i h))) :
                          𝓞 K) :
                      K)))
          i j)
      0
Tactic: rw [← det_reindex_self f.symm, det_eq_sum_row_mul_submatrix_succAbove_succAbove_det _ (f.symm w')
    (f.symm w'), abs_mul, abs_mul, abs_neg_one_pow, one_mul]