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)
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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
k : α
⊢ 0 ≤ A
have have : ∀ (l : β), 0 ≤ A
Tactic: have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
-- 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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have Apos : 0 ≤ A
Tactic: have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
-- 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
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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Apos : 0 ≤ A
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have w : β → 𝓞 K
Tactic: use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Apos : 0 ≤ A
w : β → 𝓞 K
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have left : ξ K x ≠ 0
Tactic: use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Apos : 0 ≤ A
w : β → 𝓞 K
left : ξ K x ≠ 0
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have left₁ : a *ᵥ ξ K x = 0
Tactic: use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
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‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Apos : 0 ≤ A
w : β → 𝓞 K
left : ξ K x ≠ 0
left₁ : a *ᵥ ξ K x = 0
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have right : ∀ (l : β), house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Tactic: use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
let let₁ let₂ :
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have let₃ : let 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 : ℝ))
Tactic: classical
  let h := finrank ℚ K
  have hphqh : p * h < q * h := by gcongr; exact finrank_pos
  have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
  have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
  have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
  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)
  simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
  rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
  have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
  use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
let let₁ let₂ :
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₃ :
  let 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 : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have let₄ : let 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 : ℝ))
Tactic: classical
  let h := finrank ℚ K
  have hphqh : p * h < q * h := by gcongr; exact finrank_pos
  have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
  have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
  have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
  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)
  simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
  rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
  have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
  use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
let let₁ let₂ :
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₃ :
  let 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 : ℝ))
let₄ :
  let 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 : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have let₅ : let 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 : ℝ))
Tactic: classical
  let h := finrank ℚ K
  have hphqh : p * h < q * h := by gcongr; exact finrank_pos
  have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
  have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
  have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
  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)
  simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
  rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
  have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
  use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- 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
let let₁ let₂ :
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₃ :
  let 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 : ℝ))
let₄ :
  let 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 : ℝ))
let₅ :
  let 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 : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have let₆ : let 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 : ℝ))
Tactic: classical
  let h := finrank ℚ K
  have hphqh : p * h < q * h := by gcongr; exact finrank_pos
  have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
  have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
  have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
  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)
  simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
  rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
  have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
  use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
⊢ Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ //
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
          (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C } =
    Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ //
        (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
          IsPrincipal (↑I : Ideal (𝓞 K)) ∧
            (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
              s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) }
have simp_rw : Nat.card.{u_1}
    { I : ↥(Ideal (𝓞 K))⁰ //
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
        (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C } =
  Nat.card.{u_1}
    { I : ↥(Ideal (𝓞 K))⁰ //
      J ∣ I ∧
        IsPrincipal (↑I : Ideal (𝓞 K)) ∧
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
            s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) }
Tactic: simp_rw [← nonZeroDivisors_dvd_iff_dvd_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
⊢ Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ //
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
          (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C } =
    Nat.card.{u_1}
      { I : ↥(Ideal (𝓞 K))⁰ //
        J ∣ I ∧
          IsPrincipal (↑I : Ideal (𝓞 K)) ∧
            (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
              s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) }
have refine : { I : ↥(Ideal (𝓞 K))⁰ //
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C } ≃
  { I : ↥(Ideal (𝓞 K))⁰ //
    J ∣ I ∧
      IsPrincipal (↑I : Ideal (𝓞 K)) ∧
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
          s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) }
Tactic: refine Nat.card_congr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
⊢ { I : ↥(Ideal (𝓞 K))⁰ //
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
        (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C } ≃
    { I : ↥(Ideal (𝓞 K))⁰ //
      J ∣ I ∧
        IsPrincipal (↑I : Ideal (𝓞 K)) ∧
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
            s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) }
have refine : ∀ (I : ↥(Ideal (𝓞 K))⁰),
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ↔
    IsPrincipal.{u_1, u_1} (R := 𝓞 K) (M := 𝓞 K)
        (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
              (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
                Ideal (𝓞 K))) :
          ℝ) ≤
        s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
Tactic: refine ((Equiv.dvd J).subtypeEquiv fun I ↦ ?_).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ J ∣ I) _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ↔
    IsPrincipal.{u_1, u_1} (R := 𝓞 K) (M := 𝓞 K)
        (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
          Ideal (𝓞 K)) ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
              (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
                Ideal (𝓞 K))) :
          ℝ) ≤
        s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
have rw : (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ∧
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ↔
  Eq (α := ClassGroup (𝓞 K))
      ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K))
          (Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x)
            (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
              Ideal (𝓞 K))
            sorry) :
        ClassGroup (𝓞 K))
      (1 : ClassGroup (𝓞 K)) ∧
    (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
            (↑(↑((Equiv.dvd J : (a : ↥(Ideal (𝓞 K))⁰) → { a : ↥(Ideal (𝓞 K))⁰ // J ∣ a }) I) : ↥(Ideal (𝓞 K))⁰) :
              Ideal (𝓞 K))) :
        ℝ) ≤
      s * (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
Tactic: rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]