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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k y r x_1) : 𝓞 K) (↑(x (y, r)) : 𝓞 K))
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have e_f : Eq (α := β → 𝓞 K)
  (fun (y : β) ↦
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k y r x_1) : 𝓞 K) (↑(x (y, r)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  fun (l : β) ↦
  HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
Tactic: congr 1
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
⊢ Eq (α := β → 𝓞 K)
    (fun (y : β) ↦
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k y r x_1) : 𝓞 K) (↑(x (y, r)) : 𝓞 K))
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    fun (l : β) ↦
    HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
have e_f : ∀ (r_1 : β),
  ∑ x_1 : K →+* ℂ,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r_1 r x_1) : 𝓞 K) (↑(x (r_1, r)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K) =
    HMul.hMul (α := 𝓞 K) (↑(x (r_1, r)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r_1 r u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
Tactic: ext1 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r_1 : K →+* ℂ
r : β
⊢ ∑ x_1 : K →+* ℂ,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 x_1) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K) =
    HMul.hMul (α := 𝓞 K) (↑(x (r, r_1)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
have e_f : Eq.{u_1 + 1} (α := 𝓞 K)
  (∑ x_1 : K →+* ℂ,
    HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 x_1) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  (∑ i : K →+* ℂ,
    (↑(x (r, r_1)) : 𝓞 K) *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 i) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K))
Tactic: rw [mul_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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r_1 : K →+* ℂ
r : β
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 x_1) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ i : K →+* ℂ,
      (↑(x (r, r_1)) : 𝓞 K) *
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 i) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K))
have e_f : Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
  (fun (x_1 : K →+* ℂ) ↦
    HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 x_1) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  fun (i : K →+* ℂ) ↦
  (↑(x (r, r_1)) : 𝓞 K) *
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 i) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K)
Tactic: congr 1
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r_1 : K →+* ℂ
r : β
⊢ Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
    (fun (x_1 : K →+* ℂ) ↦
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 x_1) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    fun (i : K →+* ℂ) ↦
    (↑(x (r, r_1)) : 𝓞 K) *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 i) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K)
have e_f : ∀ (r_2 : K →+* ℂ),
  HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r r_1 r_2) : 𝓞 K) (↑(x (r, r_1)) : 𝓞 K))
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r_2 : 𝓞 K) =
    (↑(x (r, r_1)) : 𝓞 K) *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r r_1 r_2) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r_2 : 𝓞 K)
Tactic: ext1 r
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
⊢ 0 = (a *ᵥ ξ K x) k
have this₁ : Eq.{u_1 + 1} (α := 𝓞 K) 0
  (∑ r : K →+* ℂ,
    ∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: have : 0 = ∑ r, ∑ l, x (l, r) * ∑ u, a' K a k l r u * (newBasis K) u := by
    conv at this => enter [2, 2, u]; rw [sum_mul]
    rw [sum_comm] at this
    rw [this]; congr 1; ext1 r
    conv => enter [1, 2, l]; rw [sum_mul]
    rw [sum_comm]; congr 1; ext1 r
    rw [mul_sum]; congr 1; ext1 r
    ring
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ r : K →+* ℂ,
      ∑ l : β,
        HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
⊢ 0 = (a *ᵥ ξ K x) k
have this₁ : Eq.{u_1 + 1} (α := 𝓞 K) 0
  (∑ y : β,
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: rw [sum_comm] at this
Cleared hypotheses: this
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
⊢ 0 = (a *ᵥ ξ K x) k
have h : ∑ y : β,
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
  (a *ᵥ ξ K x) k
Tactic: rw [this]
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
⊢ ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (a *ᵥ ξ K x) k
have h : Eq (α := β → 𝓞 K)
  (fun (y : β) ↦
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
  fun (i : β) ↦ (fun (j : β) ↦ a k j) i * ξ K x i
Tactic: congr 1
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
⊢ Eq (α := β → 𝓞 K)
    (fun (y : β) ↦
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
    fun (i : β) ↦ (fun (j : β) ↦ a k j) i * ξ K x i
have h : ∀ (l : β),
  ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (fun (j : β) ↦ a k j) l * ξ K x l
Tactic: ext1 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l : β
⊢ ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (fun (j : β) ↦ a k j) l * ξ K x l
have h : Eq.{u_1 + 1} (α := 𝓞 K)
  (∑ x_1 : K →+* ℂ,
    HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
  (∑ i : K →+* ℂ,
    (fun (j : β) ↦ a k j) l *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, i)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K))
Tactic: rw [ξ, mul_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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l : β
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
    (∑ i : K →+* ℂ,
      (fun (j : β) ↦ a k j) l *
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, i)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K))
have h : Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
  (fun (x_1 : K →+* ℂ) ↦
    HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
  fun (i : K →+* ℂ) ↦
  (fun (j : β) ↦ a k j) l *
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, i)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K)
Tactic: congr 1
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l : β
⊢ Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
    (fun (x_1 : K →+* ℂ) ↦
      HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
    fun (i : K →+* ℂ) ↦
    (fun (j : β) ↦ a k j) l *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, i)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K)
have h : ∀ (l_1 : K →+* ℂ),
  HMul.hMul (α := 𝓞 K) (↑(x (l, l_1)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l l_1 u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (fun (j : β) ↦ a k j) l *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, l_1)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l_1 : 𝓞 K)
Tactic: ext1 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l_1 : β
l : K →+* ℂ
⊢ HMul.hMul (α := 𝓞 K) (↑(x (l_1, l)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l_1 l u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (fun (j : β) ↦ a k j) l_1 *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l_1, l)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
have h : (↑(x (l_1, l)) : 𝓞 K) * HMul.hMul (β := 𝓞 K) (a k l_1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K) =
  (fun (j : β) ↦ a k j) l_1 *
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l_1, l)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
Tactic: rw [← lin_1]
-- 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)
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
⊢ ‖asiegel K a‖ ≤ c₂ K * A
have this : 0 ≤ c K
Tactic: have := c_nonneg 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)
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
⊢ ‖asiegel K a‖ ≤ c₂ K * A
have rw : ∀ (i : Prod.{u_2, u_1} α (K →+* ℂ)) (j : Prod.{u_3, u_1} β (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A
Tactic: rw [Matrix.norm_le_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)
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
rw : ∀ (i : Prod.{u_2, u_1} α (K →+* ℂ)) (j : Prod.{u_3, u_1} β (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A
⊢ ‖asiegel K a‖ ≤ c₂ K * A
have hr : 0 ≤ c₂ K * A
Tactic: rw [Matrix.norm_le_iff]