-- Module: Mathlib.NumberTheory.NumberField.CMField
Goal:
K : Type u_1
inst : Field K
inst_1 : CharZero K
inst_2 : IsCMField K
inst_3 : NumberField K
W₀ : InfinitePlace K := (Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K) w₀
f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace ↥K⁺ // w ≠ w₀ } :=
  Equiv.subtypeEquiv (p := fun (w : InfinitePlace K) ↦ w ≠ W₀) (q := fun (w : InfinitePlace ↥K⁺) ↦ w ≠ w₀)
    (equivInfinitePlace K) ⋯
g : Fin (rank K) ≃ { w : InfinitePlace K // w ≠ W₀ } := Equiv.trans (Equiv.trans (finCongr ⋯) (equivFinRank ↥K⁺)) f.symm
i w : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }
e_a :
  (↑(mult.{u_1} (K := K)
            ((Equiv.symm (equivInfinitePlace K) : (a : InfinitePlace ↥K⁺) → InfinitePlace K)
              (↑w : InfinitePlace ↥K⁺))) :
        ℝ) *
      Real.log
        (((↑w : InfinitePlace ↥K⁺) : (a : ↥K⁺) → ℝ)
          (↑(↑(fundSystem (↥K⁺)
                    ((finCongr ⋯ : (a : Fin (rank K)) → Fin (rank ↥K⁺))
                      ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K))
                        ((f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ })
                          i)))) :
                𝓞 ↥K⁺) :
            ↥K⁺)) =
    HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
      ((Matrix.of :
            (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → ℝ) →
              Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
          (fun (i : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
            (logEmbedding ↥K⁺ : (a : Additive (𝓞 ↥K⁺)ˣ) → logSpace ↥K⁺)
              ((Additive.ofMul : (a : (𝓞 ↥K⁺)ˣ) → Additive (𝓞 ↥K⁺)ˣ)
                  (fundSystem (↥K⁺)
                    (((Equiv.symm (equivFinRank ↥K⁺) : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ≃ Fin (rank.{u_1} ↥K⁺)) :
                        (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → Fin (rank ↥K⁺))
                      i)) :
                Additive (𝓞 ↥K⁺)ˣ))
          i w :
        ℝ)
⊢ Eq (α := ℝ)
    (Matrix.submatrix (m := { w : InfinitePlace K // w ≠ W₀ }) (n := { w : InfinitePlace K // w ≠ W₀ })
        ((Matrix.of :
            (a : { w : InfinitePlace K // w ≠ W₀ } → { w : InfinitePlace K // w ≠ W₀ } → ℝ) →
              Matrix { w : InfinitePlace K // w ≠ W₀ } { w : InfinitePlace K // w ≠ W₀ } ℝ)
          fun (i w : { w : InfinitePlace K // w ≠ W₀ }) ↦
          (↑(↑w : InfinitePlace K).mult : ℝ) *
            Real.log
              (((↑w : InfinitePlace K) : (a : K) → ℝ)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                    (↑(realFundSystem K ((g.symm : (a : { w : InfinitePlace K // w ≠ W₀ }) → Fin (rank K)) i)) : 𝓞 K) :
                  K)))
        (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ })
        (⇑f.symm : (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → { w : InfinitePlace K // w ≠ W₀ }) i w :
      ℝ)
    ((Matrix.of :
          (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → ℝ) →
            Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
        (fun (i j : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
          HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ)
            ((Matrix.of :
                  (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → { w : InfinitePlace ↥K⁺ // w ≠ w₀ } → ℝ) →
                    Matrix { w : InfinitePlace ↥K⁺ // w ≠ w₀ } { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ℝ)
                (fun (i : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) ↦
                  (logEmbedding ↥K⁺ : (a : Additive (𝓞 ↥K⁺)ˣ) → logSpace ↥K⁺)
                    ((Additive.ofMul : (a : (𝓞 ↥K⁺)ˣ) → Additive (𝓞 ↥K⁺)ˣ)
                        (fundSystem (↥K⁺)
                          (((Equiv.symm (equivFinRank ↥K⁺) :
                                { w : InfinitePlace ↥K⁺ // w ≠ w₀ } ≃ Fin (rank.{u_1} ↥K⁺)) :
                              (a : { w : InfinitePlace ↥K⁺ // w ≠ w₀ }) → Fin (rank ↥K⁺))
                            i)) :
                      Additive (𝓞 ↥K⁺)ˣ))
                i j :
              ℝ))
        i w :
      ℝ)

Tactic:
rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]

Premises used: NumberField.IsCMField.equivInfinitePlace_symm_apply, Matrix.of_apply, Matrix.submatrix_apply