-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_le_bound : ∀ l, house (ξ K x l).1 ≤ (c₁ K) *
    ((c₁ K * q * A)^((p : ℝ) / (q - p)))

Proof state:
case calc_5.c0
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ 0 ≤ (↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))

Tactic:
apply Real.rpow_nonneg

Result:
case calc_5.c0.hx
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ 0 ≤ ↑q * ↑h * ‖NumberField.house.asiegel K a‖

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ house ↑(NumberField.house.ξ K x l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑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))) := ?_

Result:
case calc_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ house ((algebraMap (𝓞 K) K) (∑ r : K →+* ℂ, ↑(x (l, r)) * (NumberField.house.newBasis K) r)) ≤
    ∑ r : K →+* ℂ, house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ∑ r : K →+* ℂ, house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ∑ r : K →+* ℂ, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ∑ r : K →+* ℂ, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ∑ r : K →+* ℂ, ‖x (l, r)‖ * NumberField.house.supOfBasis K

case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ∑ r : K →+* ℂ, ‖x (l, r)‖ * NumberField.house.supOfBasis K ≤
    ∑ _r : K →+* ℂ, (↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p)) * NumberField.house.supOfBasis K

case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ∑ _r : K →+* ℂ, (↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p)) * NumberField.house.supOfBasis K ≤
    ↑h * NumberField.house.c₂ K * (↑q * NumberField.house.c₁ K * A) ^ (↑p / (↑q - ↑p))

case calc_6
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ↑h * NumberField.house.c₂ K * (↑q * NumberField.house.c₁ K * A) ^ (↑p / (↑q - ↑p)) ≤
    NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Proof state:
case calc_5.h₂.h₁
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ↑q * ↑h * ‖NumberField.house.asiegel K a‖ ≤ ↑q * ↑(finrank ℚ K) * (NumberField.house.c₂ K * A)

Tactic:
apply mul_le_mul_of_nonneg_left (asiegel_remark K a habs Apos)
  (mul_nonneg (Nat.cast_nonneg' _) (Nat.cast_nonneg _))

Result:
no goals

Proof state:
case h.e'_4.h.e'_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ‖x (l, r)‖ = house ((algebraMap (𝓞 K) K) ↑(x (l, r)))

Tactic:
simp only [map_intCast, house_intCast, Int.cast_abs, Int.norm_eq_abs]

Result:
no goals