-- 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')))
i j : Fin (rank K)
e_a :
  (↑(mult.{u_1} (K := K) (↑((g.symm : (a : Fin (rank K)) → { w : InfinitePlace K // w ≠ w' }) j) : InfinitePlace K)) :
        ℝ) *
      Real.log
        (((↑((g.symm : (a : Fin (rank K)) → { w : InfinitePlace K // w ≠ w' }) j) : InfinitePlace K) : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              (↑(u
                    ((e : (a : { w : InfinitePlace K // w ≠ w' }) → Fin (rank K))
                      ((g.symm : (a : Fin (rank K)) → { w : InfinitePlace K // w ≠ w' }) i))) :
                𝓞 K) :
            K)) =
    (↑(mult.{u_1} (K := K)
            ((f : (a : Fin (rank K + 1)) → InfinitePlace K)
              (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') j))) :
        ℝ) *
      Real.log
        ((((f : (a : Fin (rank K + 1)) → InfinitePlace K)
                (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') j) :
              InfinitePlace K) :
            (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')
                        ((f : (a : Fin (rank K + 1)) → InfinitePlace K)
                          (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') i))
                        ⋯))) :
                𝓞 K) :
            K))
⊢ Eq (α := ℝ)
    (((reindex g g :
            Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ ≃
              Matrix (Fin (rank K)) (Fin (rank K)) ℝ) :
          (a : Matrix { w : InfinitePlace K // w ≠ w' } { w : InfinitePlace K // w ≠ w' } ℝ) →
            Matrix (Fin (rank K)) (Fin (rank K)) ℝ)
        ((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)))
        i j :
      ℝ)
    (submatrix (m := InfinitePlace K) (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) ℝ)
        (fun (x : Fin (rank K)) ↦
          ((f : (a : Fin (rank K + 1)) → InfinitePlace K)
              (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') x) :
            InfinitePlace K))
        (fun (x : Fin (rank K)) ↦
          ((f : (a : Fin (rank K + 1)) → InfinitePlace K)
              (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') x) :
            InfinitePlace K))
        i j :
      ℝ)
have e_a₁ : ¬(f : (a : Fin (rank K + 1)) → InfinitePlace K)
      (Fin.succAbove ((f.symm : (a : InfinitePlace K) → Fin (rank K + 1)) w') i) =
    w'
Tactic: rw [reindex_apply, submatrix_apply, submatrix_apply, of_apply, of_apply, dif_neg]