-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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))) :
      ℝ)
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)) :
      ℝ)
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) (1 : 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)) :
      ℝ)
rw₅ 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) → ℝ)
        ((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)) :
      ℝ)

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]

Premises used: Exists.choose_spec, Algebra.algebraMap, mul_assoc, NumberField.Units.dirichletUnitTheorem.seq_ne_zero, congr_arg, map_mul, mul_comm, NumberField.RingOfIntegers, DFunLike.coe, inv_mul_cancel₀, one_mul