awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
⊢ 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)) ≤
    house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K) *
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)

Tactic:
house_mul_le ..

Premises used: NumberField.house_mul_le
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
h₁ : ‖x (l, r)‖ = house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : 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)) ≤
    ‖x (l, r)‖ * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)

Tactic:
convert! house_mul_le ..

Premises used: NumberField.house_mul_le
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
⊢ ‖x (l, r)‖ = house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)

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

Premises used: Int.cast_abs, NumberField.house_intCast, map_intCast, Int.norm_eq_abs
-- 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_3 :
  ∀ (r : K →+* ℂ),
    Membership.mem (γ := Finset (K →+* ℂ)) univ r →
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K) ≤
        sup' univ ⋯ fun (r : K →+* ℂ) ↦
          house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
⊢ 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)‖ *
        sup' univ ⋯ fun (r : K →+* ℂ) ↦
          house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))

Tactic:
gcongr with r _
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
calc_3 :
  ∃ (b : K →+* ℂ),
    house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K) ≤
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) : K)
⊢ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K) ≤
    sup' univ ⋯ fun (r : K →+* ℂ) ↦
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)

Tactic:
simp only [le_sup'_iff, mem_univ, true_and]

Premises used: Finset.mem_univ, Finset.le_sup'_iff, true_and
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
w : K →+* ℂ
h₁ :
  house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K) ≤
    house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
⊢ ∃ (b : K →+* ℂ),
    house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K) ≤
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) : K)

Tactic:
use r
-- 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_4 :
  ∀ (r : K →+* ℂ),
    Membership.mem (γ := Finset (K →+* ℂ)) univ r →
      ‖x (l, r)‖ ≤
        (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ 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)

Tactic:
gcongr with r _
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
⊢ ‖x (l, r)‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
le_trans (norm_le_pi_norm x ⟨l, r⟩) hxbound

Premises used: norm_le_pi_norm, Prod.mk, le_trans
-- 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 : ℝ)
r : K →+* ℂ
h_1 : Membership.mem (γ := Finset (K →+* ℂ)) univ r
⊢ ‖x (l, r)‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
exact le_trans (norm_le_pi_norm x ⟨l, r⟩) hxbound

Premises used: norm_le_pi_norm, Prod.mk, le_trans
-- 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_5 :
  (↑(Fintype.card.{u_1} (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 : ℝ))
⊢ ∑ _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 : ℝ))

Tactic:
simp only [sum_const, card_univ, nsmul_eq_mul]

Premises used: Finset.card_univ, nsmul_eq_mul, Finset.sum_const
-- 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_5 :
  (↑(finrank ℚ K) : ℝ) * supOfBasis K *
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    (↑h : ℝ) * (max 1 (c K) * supOfBasis K) *
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * (c₂ K * A)) ^
        ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ (↑(Fintype.card.{u_1} (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 : ℝ))

Tactic:
rw [Embeddings.card, mul_comm _ (supOfBasis K), c₂, c₁, ← mul_assoc,
      ← mul_assoc (q : ℝ), mul_assoc (q * _ : ℝ)]

Premises used: HMul.hMul, mul_assoc, NumberField.Embeddings.card, _private.0.NumberField.house.supOfBasis, Nat.cast, mul_comm, _private.0.NumberField.house.c₂, _private.0.NumberField.house.c₁
-- 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_5 : supOfBasis K ≤ max 1 (c K) * supOfBasis K
calc_5₁ : ‖asiegel K a‖ ≤ c₂ K * A
⊢ (↑(finrank ℚ K) : ℝ) * supOfBasis K *
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    (↑h : ℝ) * (max 1 (c K) * supOfBasis K) *
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * (c₂ K * A)) ^
        ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
gcongr
-- 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 : ℝ)
⊢ supOfBasis K ≤ max 1 (c K) * supOfBasis K

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

Premises used: le_mul_of_one_le_left, _private.0.NumberField.house.supOfBasis_nonneg, le_max_left
-- 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 : ℝ)
⊢ supOfBasis K ≤ max 1 (c K) * supOfBasis K

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

Premises used: le_mul_of_one_le_left, _private.0.NumberField.house.supOfBasis_nonneg, le_max_left
-- 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 : ℝ)
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
asiegel_remark K a habs Apos

Premises used: _private.0.NumberField.house.asiegel_remark
-- 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 : ℝ)
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
exact asiegel_remark K a habs Apos

Premises used: _private.0.NumberField.house.asiegel_remark
-- 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_6 :
  (↑h : ℝ) * c₂ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    (↑h : ℝ) * c₂ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

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

Premises used: Nat.cast, mul_comm, _private.0.NumberField.house.c₁
-- 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 : ℝ)
⊢ (↑h : ℝ) * c₂ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    (↑h : ℝ) * c₂ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
rfl
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
ha₁ : 0 < h
⊢ p * h < q * h

Tactic:
gcongr
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
⊢ 0 < h

Tactic:
finrank_pos

Premises used: Module.finrank_pos
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
⊢ 0 < h

Tactic:
exact finrank_pos

Premises used: Module.finrank_pos
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
⊢ p * h < q * h

Tactic:
have hphqh : p * h < q * h := by gcongr; exact finrank_pos
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
rw : 0 < p ∧ 0 < h ∨ p < 0 ∧ h < 0
⊢ 0 < p * h

Tactic:
rw [mul_pos_iff]

Premises used: mul_pos_iff
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h₁ : 0 < p ∧ 0 < h
⊢ 0 < p ∧ 0 < h ∨ p < 0 ∧ h < 0

Tactic:
constructor
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
⊢ 0 < p ∧ 0 < h

Tactic:
⟨h0p, finrank_pos⟩

Premises used: And.intro, Module.finrank_pos
-- 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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
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 α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
⊢ 0 < p ∧ 0 < h

Tactic:
exact ⟨h0p, finrank_pos⟩