-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : realSpace K
conv_rhs :
  (HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))) =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))
conv_rhs₁ :
  (HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))) =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))
⊢ (HSMul.hSMul (β := (w : InfinitePlace K) → ℝ) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (x (↑i : InfinitePlace K))) =
    HSMul.hSMul (β := realSpace K) (Real.exp (x w₀)) fun (w : InfinitePlace K) ↦
      ∏ i : { w : InfinitePlace K // w ≠ w₀ },
        HPow.hPow (α := ℝ)
          ((w : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                  (↑(fundSystem K
                        (((Equiv.symm equivFinRank : { w : InfinitePlace K // w ≠ w₀ } ≃ Fin (rank K)) :
                            (a : { w : InfinitePlace K // w ≠ w₀ }) → Fin (rank K))
                          i)) :
                    𝓞 K) :
                K) :
            ℝ)
          (if (↑i : InfinitePlace K) = w₀ then 0 else x (↑i : InfinitePlace K))

Tactic:
conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]