-- 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_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))

Tactic:
rw [mul_comm (q : ℝ) (c₁ K)]

Result:
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 * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p)) ≤
    NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Proof state:
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 : β
⊢ ↑(finrank ℚ K) * NumberField.house.supOfBasis K * (↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * ((1 ⊔ NumberField.house.c K) * NumberField.house.supOfBasis K) *
      (↑q * (↑(finrank ℚ K) * NumberField.house.c₂ K) * A) ^ (↑p / (↑q - ↑p))

Tactic:
apply mul_le_mul

Result:
case calc_5.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 : β
⊢ ↑(finrank ℚ K) * NumberField.house.supOfBasis K ≤ ↑h * ((1 ⊔ NumberField.house.c K) * NumberField.house.supOfBasis K)

case calc_5.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‖) ^ (↑p / (↑q - ↑p)) ≤
    (↑q * (↑(finrank ℚ K) * NumberField.house.c₂ K) * A) ^ (↑p / (↑q - ↑p))

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))

case calc_5.b0
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 ≤ ↑h * ((1 ⊔ NumberField.house.c K) * NumberField.house.supOfBasis K)

Proof state:
case calc_3.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 : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ‖x (l, r)‖ * NumberField.house.supOfBasis K

Tactic:
unfold supOfBasis

Result:
case calc_3.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 : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ‖x (l, r)‖ * univ.sup' ⋯ fun r => house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

Proof state:
case calc_2.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 : β
⊢ ∀ i ∈ univ,
    house ((algebraMap (𝓞 K) K) ↑(x (l, i)) * (algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) i)) ≤
      ‖x (l, i)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) i))

Tactic:
intros r _

Result:
case calc_2.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 : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

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 : β
⊢ NumberField.house.supOfBasis K ≤ (1 ⊔ NumberField.house.c K) * NumberField.house.supOfBasis K

Tactic:
exact le_mul_of_one_le_left (supOfBasis_nonneg K) (le_max_left ..)

Result:
no goals