-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < (↑(convexBodyLTFactor K) : ENNReal) * (↑B : ENNReal)
n m : ℕ
hnm : n < m
h : Eq (α := Ideal (𝓞 K)) (Ideal.span {(↑(seq K w₁ hB n) : 𝓞 K)}) (Ideal.span {(↑(seq K w₁ hB m) : 𝓞 K)})
hu : Associated (↑(seq K w₁ hB n) : 𝓞 K) (↑(seq K w₁ hB m) : 𝓞 K)
w : InfinitePlace K
hw : w ≠ w₁
rw :
  Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              ((↑(seq K w₁ hB n) : 𝓞 K) *
                (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                      (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                  𝓞 K)) :
            K)
          (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
      ℝ)
rw₁ :
  Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
              ((↑(seq K w₁ hB n) : 𝓞 K) *
                (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                      (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                  𝓞 K)) :
            K)) :
      ℝ)
rw₂ :
  Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)
          (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦
                      (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K)) hu) :
                  𝓞 K) :
              K))) :
      ℝ)
⊢ Eq (α := ℝ)
    ((w : (a : K) → ℝ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K) :
      ℝ)
    ((w : (a : K) → ℝ)
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB m) : 𝓞 K) : K)
          (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)) :
      ℝ)
have rw₃ : Eq (α := ℝ)
  ((w : (a : K) → ℝ)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                hu) :
            𝓞 K) :
        K) :
    ℝ)
  ((w : (a : K) → ℝ)
      (HMul.hMul (β := K)
        (HMul.hMul (α := K) (β := K) (((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K))⁻¹ : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(seq K w₁ hB n) : 𝓞 K) : K))
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(Exists.choose (p := fun (u : (𝓞 K)ˣ) ↦ (↑(seq K w₁ hB n) : 𝓞 K) * (↑u : 𝓞 K) = (↑(seq K w₁ hB m) : 𝓞 K))
                  hu) :
              𝓞 K) :
          K)) :
    ℝ)
Tactic: rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _),
          ← mul_assoc, inv_mul_cancel₀ (seq_ne_zero K w₁ hB n), one_mul]