-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a k l) : K) ≤ A
inst_3 : DecidableEq (K →+* ℂ)
inst_4 : Fintype α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
calc_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
calc_2 :
  LE.le (α := ℝ)
    (∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
calc_3 :
  LE.le (α := ℝ)
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
    (∑ r : K →+* ℂ, ‖x (l, r)‖ * supOfBasis K)
calc_4 :
  LE.le (α := ℝ) (∑ r : K →+* ℂ, ‖x (l, r)‖ * supOfBasis K)
    (∑ _r : K →+* ℂ,
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) *
        supOfBasis K)
calc_5 :
  ∑ _r : K →+* ℂ,
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) *
        supOfBasis K ≤
    (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
calc_6 :
  (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_

Premises used: Norm.norm, Int.cast, HMul.hMul, Finset.univ, _private.0.NumberField.house.newBasis, _private.0.NumberField.house.asiegel, Algebra.algebraMap, HSub.hSub, HDiv.hDiv, Prod.mk, _private.0.NumberField.house.supOfBasis, Nat.cast, HPow.hPow, NumberField.house, _private.0.NumberField.house.c₂, NumberField.RingOfIntegers, DFunLike.coe, _private.0.NumberField.house.c₁, Finset.sum, rfl