-- Mathlib/NumberTheory/NumberField/Units/Regulator.lean
theorem finrank_mul_regulator_eq_det (w' : InfinitePlace K) (e : {w // w ≠ w'} ≃ Fin (rank K)) :
    finrank ℚ K * regulator K =
      |(Matrix.of (fun i w : InfinitePlace K ↦
        if h : i = w' then (w.mult : ℝ) else w.mult * (w (fundSystem K (e ⟨i, h⟩))).log)).det|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
b✝ : InfinitePlace K
h : ¬b✝ = w'
⊢ (if h : b✝ = w' then ∑ x : InfinitePlace K, ↑x.mult
    else ∑ x : InfinitePlace K, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨b✝, ⋯⟩))))) =
    0

Tactic:
rw [dif_neg h, sum_mult_mul_log]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
x✝ : InfinitePlace K
⊢ x✝ ≠ w' ↔ f.symm x✝ ≠ f.symm w'

Tactic:
simp [f]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j : Fin (rank K + 1),
          (Matrix.reindex f.symm f.symm)
            (Matrix.of fun i w =>
              if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩)))))
            i j =
        0

Tactic:
simp_rw [Equiv.forall_congr_left f, ← f.symm.sum_comp, Matrix.reindex_apply,
  Matrix.submatrix_apply, Matrix.of_apply, f.symm_symm, f.apply_symm_apply,
  Finset.sum_dite_irrel, ne_eq, EmbeddingLike.apply_eq_iff_eq]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (b : InfinitePlace K),
    ¬b = w' →
      (if h : b = w' then ∑ x : InfinitePlace K, ↑x.mult
        else ∑ x : InfinitePlace K, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨b, ⋯⟩))))) =
        0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
rw [← Matrix.det_reindex_self f.symm, Matrix.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]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ↑(finrank ℚ K) * regulator K =
    |∑ j : Fin (rank K + 1),
          (Matrix.reindex f.symm f.symm)
            (Matrix.of fun i w =>
              if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩)))))
            (f.symm w') j| *
      |(((Matrix.reindex f.symm f.symm)
                (Matrix.of fun i w =>
                  if h : i = w' then ↑w.mult
                  else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩)))))).submatrix
            (f.symm w').succAbove (f.symm w').succAbove).det|

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (i : Fin (rank K + 1)),
    i ≠ f.symm w' →
      ∑ j : Fin (rank K + 1),
          (Matrix.reindex f.symm f.symm)
            (Matrix.of fun i w =>
              if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩)))))
            i j =
        0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Tactic:
let f : Fin (rank K + 1) ≃ InfinitePlace K :=
  (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e.symm).val

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
⊢ ↑(finrank ℚ K) * regulator K =
    |(Matrix.of fun i w =>
          if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨i, h⟩))))).det|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
⊢ ∀ (b : InfinitePlace K),
    ¬b = w' →
      (if h : b = w' then ∑ x : InfinitePlace K, ↑x.mult
        else ∑ x : InfinitePlace K, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨b, ⋯⟩))))) =
        0

Tactic:
intro _ h

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
b✝ : InfinitePlace K
h : ¬b✝ = w'
⊢ (if h : b✝ = w' then ∑ x : InfinitePlace K, ↑x.mult
    else ∑ x : InfinitePlace K, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(fundSystem K (e ⟨b✝, ⋯⟩))))) =
    0