-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
_ :
  norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
_₁ :
  LE.le (α := ℝ)
    (∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
    (∑ j : K →+* ℂ,
      norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
_₂ :
  LE.le (α := ℝ)
    (∑ j : K →+* ℂ,
      norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
    (∑ x : K →+* ℂ,
      (norm.{u_1} (E := (i j : K →+* ℂ) → ℂ) fun (i j : K →+* ℂ) ↦ (basisMatrix K)ᵀ⁻¹ i j) *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K))
_₃ :
  ∑ x : K →+* ℂ,
      (norm.{u_1} (E := (i j : K →+* ℂ) → ℂ) fun (i j : K →+* ℂ) ↦ (basisMatrix K)ᵀ⁻¹ i j) *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) =
    (↑(finrank ℚ K) : ℝ) * norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
⊢ norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)

Tactic:
calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]

Premises used: Algebra.algebraMap, Rat, Inv.inv, Matrix.transpose, NumberField.house, NumberField.RingOfIntegers, DFunLike.coe, Module.finrank, NumberField.basisMatrix