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

Tactic:
have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, 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
h0ph : 0 < p * h
rw : Fintype.card α * Fintype.card.{u_1} (K →+* ℂ) = p * h
rw₁ : p * Fintype.card.{u_1} (K →+* ℂ) = p * h
rw₂ rw₃ : p * finrank ℚ K = p * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h

Tactic:
rw [Fintype.card_prod, cardα, Embeddings.card]

Premises used: NumberField.Embeddings.card, Fintype.card_prod
-- 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
h0ph : 0 < p * h
⊢ 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]
-- 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
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
rw₂ rw₃ : q * finrank ℚ K = q * h
⊢ Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h

Tactic:
rw [Fintype.card_prod, cardβ, Embeddings.card]

Premises used: NumberField.Embeddings.card, Fintype.card_prod
-- 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
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

Tactic:
have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
-- 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
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
rwa : p * h < Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))
rwa₁ rwa₂ rwa₃ rwa₄ : p * h < q * h
⊢ Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) < Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))

Tactic:
rwa [hfinp, hfinq]
-- 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
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
rwa rwa₁ rwa₂ rwa₃ : 0 < p * h
⊢ 0 < Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))

Tactic:
rwa [hfinp]
-- 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
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
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 : ℝ))
⊢ ∃ (ξ : β → 𝓞 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)
-- 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
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 →+* ℂ))) : ℝ))
⊢ ‖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

Premises used: Nat.cast_mul
-- 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
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 : ℝ)))
⊢ ‖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

Premises used: mul_div_mul_right, sub_mul
-- 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
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 : α
have : ∀ (l : β), 0 ≤ A
⊢ 0 ≤ A

Tactic:
have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
-- 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
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 : α
l : β
⊢ 0 ≤ A

Tactic:
le_trans (house_nonneg _) (habs k l)

Premises used: NumberField.house_nonneg, 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)
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 : α
l : β
⊢ 0 ≤ A

Tactic:
exact le_trans (house_nonneg _) (habs k l)

Premises used: NumberField.house_nonneg, 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)
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 : ℝ))
⊢ 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)
-- 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
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
right :
  ∀ (l : β), house (↑(ξ K x 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 : ℝ))

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

Premises used: _private.0.NumberField.house.ξ_ne_0, _private.0.NumberField.house.ξ_mulVec_eq_0, _private.0.NumberField.house.house_le_bound, _private.0.NumberField.house.ξ
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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⁻¹
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))) : ℝ) }
⊢ 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))) : ℝ) }

Tactic:
simp_rw [← nonZeroDivisors_dvd_iff_dvd_coe]

Premises used: nonZeroDivisors_dvd_iff_dvd_coe
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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))) : ℝ) }

Tactic:
Nat.card_congr ?_

Premises used: Nat.card_congr
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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⁻¹
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))) : ℝ) }
⊢ 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:
refine Nat.card_congr ?_

Premises used: Nat.card_congr
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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⁻¹
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))) : ℝ)
⊢ { 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 ((Equiv.dvd J).subtypeEquiv fun I ↦ ?_).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter (fun I : (Ideal (𝓞 K))⁰ ↦ J ∣ I) _)

Premises used: Dvd.dvd, Equiv.trans, Equiv.dvd, Equiv.subtypeEquiv, Equiv.subtypeSubtypeEquivSubtypeInter
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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))⁰
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))
              ⋯) :
          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))) : ℝ)
⊢ (↑((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:
rw [← ClassGroup.mk0_eq_one_iff (SetLike.coe_mem _)]

Premises used: SetLike.coe_mem, ClassGroup.mk0_eq_one_iff
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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))⁰
simp_rw :
  C = (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I →
    ((↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ↔
      HMul.hMul (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) * s)
⊢ (↑((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))
              ⋯) :
          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:
simp_rw [Equiv.dvd_apply, Submonoid.coe_mul, ← Submonoid.mul_def, _root_.map_mul, hJ,
    inv_mul_eq_one, Nat.cast_mul, mul_comm s, eq_comm, and_comm, and_congr_left_iff]

Premises used: and_comm, eq_comm, map_mul, Nat.cast_mul, Submonoid.mul_def, and_congr_left_iff, mul_comm, Equiv.dvd_apply, Submonoid.coe_mul, inv_mul_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics
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))⁰
⊢ C = (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I →
    ((↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s ↔
      HMul.hMul (α := ℝ) (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ)
          (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑J : Ideal (𝓞 K))) : ℝ) * s)

Tactic:
fun _ ↦
    (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm

Premises used: Iff.mpr, Nat.cast_pos, mul_le_mul_iff_of_pos_left, Ideal.absNorm_pos_of_nonZeroDivisors, Iff.symm