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)
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 →+* ℂ
h :
  ∀ (l : K →+* ℂ),
    ∑ i : β,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
| Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 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)))

Tactic:
enter [1, 2, l]; rw [sum_mul]

Premises used: Finset.sum_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)
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 →+* ℂ
e_f :
  Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ l : K →+* ℂ,
      ∑ i : β,
        HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 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)))
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 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)))

Tactic:
conv => enter [1, 2, l]; rw [sum_mul]

Premises used: Finset.sum_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)
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 →+* ℂ
e_f :
  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)))
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ l : K →+* ℂ,
      ∑ i : β,
        HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 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:
rw [sum_comm]

Premises used: Finset.sum_comm
-- 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)
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 →+* ℂ
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))
⊢ 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)))

Tactic:
congr 1
-- 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)
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 →+* ℂ
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))
⊢ 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:
ext1 r
-- 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)
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 : β
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))
⊢ ∑ 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))

Tactic:
rw [mul_sum]

Premises used: Finset.mul_sum
-- 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)
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 : β
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)
⊢ 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:
congr 1
-- 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)
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 : β
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)
⊢ 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:
ext1 r
-- 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)
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_2 : β
r : K →+* ℂ
⊢ HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k r_2 r_1 r) : 𝓞 K) (↑(x (r_2, r_1)) : 𝓞 K))
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) =
    (↑(x (r_2, r_1)) : 𝓞 K) *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k r_2 r_1 r) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)

Tactic:
ring
-- 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)
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))
⊢ 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
-- 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)
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)))
⊢ 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

Premises used: Finset.sum_comm
-- 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)
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)))
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
⊢ 0 = (a *ᵥ ξ K x) k

Tactic:
rw [this]
-- 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)
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)))
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
⊢ ∑ 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:
congr 1
-- 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)
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)))
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
⊢ 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:
ext1 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)
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 : β
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))
⊢ ∑ 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:
rw [ξ, mul_sum]

Premises used: Finset.mul_sum, _private.0.NumberField.house.ξ
-- 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)
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 : β
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)
⊢ 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:
congr 1