awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 (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)
have 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)
Tactic: simp only [le_sup'_iff, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 →+* ℂ
⊢ ∃ (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)
have 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)
Tactic: use r
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 : ℝ)
⊢ 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)
have 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 : ℝ))
Tactic: gcongr with r _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 →+* ℂ,
      (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 : ℝ))
have 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 : ℝ))
Tactic: simp only [sum_const, card_univ, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 : ℝ)
⊢ (↑(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 : ℝ))
have 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 : ℝ))
Tactic: rw [Embeddings.card, mul_comm _ (supOfBasis K), c₂, c₁, ← mul_assoc,
      ← mul_assoc (q : ℝ), mul_assoc (q * _ : ℝ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 : ℝ)
⊢ (↑(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 : ℝ))
have calc_5 : supOfBasis K ≤ max 1 (c K) * supOfBasis K
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
⊢ (↑(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 : ℝ))
have calc_5₁ : ‖asiegel K a‖ ≤ c₂ K * A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have 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 : ℝ))
Tactic: rw [mul_comm (q : ℝ) (c₁ K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
have ha₁ : 0 < h
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have hphqh : p * h < q * h
Tactic: have hphqh : p * h < q * h := by gcongr; exact finrank_pos
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 * h
have rw : 0 < p ∧ 0 < h ∨ p < 0 ∧ h < 0
Tactic: rw [mul_pos_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 ∨ p < 0 ∧ h < 0
have h₁ : 0 < p ∧ 0 < h
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have h0ph : 0 < p * h
Tactic: have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
have rw : Fintype.card α * Fintype.card.{u_1} (K →+* ℂ) = p * h
Tactic: rw [Fintype.card_prod, cardα, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
rw : Fintype.card α * Fintype.card.{u_1} (K →+* ℂ) = p * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
have rw₁ : p * Fintype.card.{u_1} (K →+* ℂ) = p * h
Tactic: rw [Fintype.card_prod, cardα, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
rw : Fintype.card α * Fintype.card.{u_1} (K →+* ℂ) = p * h
rw₁ : p * Fintype.card.{u_1} (K →+* ℂ) = p * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
have rw₂ : p * finrank ℚ K = p * h
Tactic: rw [Fintype.card_prod, cardα, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
h0ph : 0 < p * h
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
Tactic: have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
⊢ Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
have rw : Fintype.card β * Fintype.card.{u_1} (K →+* ℂ) = q * h
Tactic: rw [Fintype.card_prod, cardβ, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
rw : Fintype.card β * Fintype.card.{u_1} (K →+* ℂ) = q * h
⊢ Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
have rw₁ : q * Fintype.card.{u_1} (K →+* ℂ) = q * h
Tactic: rw [Fintype.card_prod, cardβ, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
rw : Fintype.card β * Fintype.card.{u_1} (K →+* ℂ) = q * h
rw₁ : q * Fintype.card.{u_1} (K →+* ℂ) = q * h
⊢ Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
have rw₂ : q * finrank ℚ K = q * h
Tactic: rw [Fintype.card_prod, cardβ, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
Tactic: have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) < Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))
have rwa : p * h < Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))
Tactic: rwa [hfinp, hfinq]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have have : ∀ (x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ) (hxl : x ≠ 0) (hmulvec0 : asiegel K a *ᵥ x = 0)
  (hxbound :
    ‖x‖ ≤
      ((↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ) * ‖asiegel K a‖) ^
        ((↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ) /
          HSub.hSub (α := ℝ) (↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ)
            (↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ))),
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Tactic: have ⟨x, hxl, hmulvec0, hxbound⟩ :=
    Int.Matrix.exists_ne_zero_int_vec_norm_le' (asiegel K a)
      (by rwa [hfinp, hfinq]) (by rwa [hfinp]) (asiegel_ne_0 K a ha)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound :
  ‖x‖ ≤
    ((↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ) * ‖asiegel K a‖) ^
      ((↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ) /
        HSub.hSub (α := ℝ) (↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ)
          (↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have hxbound₁ : ‖x‖ ≤
  (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^
    (HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ) /
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) - HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ)))
Tactic: simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
Cleared hypotheses: hxbound
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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
h0ph : 0 < p * h
hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h
hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^
      (HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ) /
        (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) - HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ)))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have hxbound₁ : ‖x‖ ≤ (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Tactic: rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
Cleared hypotheses: hxbound