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)
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
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A
have calc_6 : c K * supOfBasis K * A ≤ max 1 (c K) * supOfBasis K * A
Tactic: rw [mul_right_comm, c₂]
-- 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)
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
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ c K * supOfBasis K * A ≤ max 1 (c K) * supOfBasis K * A
have calc_6 : 0 ≤ 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)
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
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_6 : 0 ≤ supOfBasis K
⊢ c K * supOfBasis K * A ≤ max 1 (c K) * supOfBasis K * A
have calc_6₁ : c K ≤ max 1 (c K)
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)
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 : β
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have H₀ : 0 ≤ supOfBasis K
Tactic: have H₀ : 0 ≤ NumberField.house.supOfBasis K := supOfBasis_nonneg _
-- 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)
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
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
Tactic: have H₁ : 0 < (q - p : ℝ) := sub_pos.mpr <| mod_cast hpq
-- 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 : ℝ)
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_1 : house (K := K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (∑ r : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
      K) ≤
  ∑ r : 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))
Tactic: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_2 : LE.le (α := ℝ)
  (∑ r : 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)))
  (∑ r : K →+* ℂ,
    ‖x (l, r)‖ * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
Tactic: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
calc_2 :
  LE.le (α := ℝ)
    (∑ r : 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)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_3 : 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)‖ * supOfBasis K)
Tactic: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
calc_2 :
  LE.le (α := ℝ)
    (∑ r : 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)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
calc_3 :
  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)‖ * supOfBasis K)
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_4 : 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: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
calc_2 :
  LE.le (α := ℝ)
    (∑ r : 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)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
calc_3 :
  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)‖ * supOfBasis K)
calc_4 :
  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)
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_5 : ∑ _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: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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_1 :
  house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
calc_2 :
  LE.le (α := ℝ)
    (∑ r : 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)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
calc_3 :
  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)‖ * supOfBasis K)
calc_4 :
  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)
calc_5 :
  ∑ _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 : ℝ))
⊢ house (↑(ξ K x l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
have calc_6 : (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
  c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
Tactic: calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
-- 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 : ℝ)
⊢ house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : 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))
have calc_1 : house.{u_1} (K := K)
    (∑ x_1 : K →+* ℂ,
      (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
        (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))) ≤
  ∑ x_1 : K →+* ℂ,
    house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K)) :
        K)
Tactic: simp_rw [← map_mul, map_sum]
-- 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 →+* ℂ,
      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)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
have calc_2 : ∀ (r : K →+* ℂ),
  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)) ≤
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
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 →+* ℂ
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)) ≤
    ‖x (l, r)‖ * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
have h₁ : ‖x (l, r)‖ = house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
Tactic: convert! house_mul_le ..
-- 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)‖ *
        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))
have 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 sorry fun (r : K →+* ℂ) ↦
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
Tactic: gcongr with r _