-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne (goal)
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))
⊢ (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))
have 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))
Tactic: conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]