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_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
⊢ LinearIndependent (ι := K →+* ℂ) ℤ (M := 𝓞 K) (⇑(newBasis K) : (a : K →+* ℂ) → 𝓞 K)

Tactic:
have hblin := Basis.linearIndependent (newBasis K)
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : LinearIndependent (ι := K →+* ℂ) ℤ (M := 𝓞 K) (⇑(newBasis K) : (a : K →+* ℂ) → 𝓞 K)
⊢ ∀ (g : (K →+* ℂ) → ℤ),
    Eq.{u_1 + 1} (α := 𝓞 K)
        (∑ x : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(g x) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x : 𝓞 K))
        0 →
      ∀ (i : K →+* ℂ), g i = 0

Tactic:
simp only [zsmul_eq_mul, Fintype.linearIndependent_iff] at hblin

Premises used: zsmul_eq_mul, Fintype.linearIndependent_iff
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin :
  ∀ (g : (K →+* ℂ) → ℤ),
    Eq.{u_1 + 1} (α := 𝓞 K)
        (∑ x : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(g x) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x : 𝓞 K))
        0 →
      ∀ (i : K →+* ℂ), g i = 0
⊢ x (l, r) = 0 (l, r)

Tactic:
hblin (fun r ↦ x (l, r)) (H _) r

Premises used: Prod.mk
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin :
  ∀ (g : (K →+* ℂ) → ℤ),
    Eq.{u_1 + 1} (α := 𝓞 K)
        (∑ x : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(g x) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x : 𝓞 K))
        0 →
      ∀ (i : K →+* ℂ), g i = 0
⊢ x (l, r) = 0 (l, r)

Tactic:
exact hblin (fun r ↦ x (l, r)) (H _) r

Premises used: Prod.mk
-- 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)
l : β
k : α
r : K →+* ℂ
⊢ HMul.hMul (β := 𝓞 K) (a k l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) 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:
simp only [Basis.sum_repr (newBasis K) (a k l * (newBasis K) r), a', ← zsmul_eq_mul]

Premises used: zsmul_eq_mul, HMul.hMul, _private.0.NumberField.house.newBasis, _private.0.NumberField.house.a', DFunLike.coe, Module.Basis.sum_repr
-- 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
h : ∀ (k : α), (a *ᵥ ξ K x) k = 0 k
⊢ a *ᵥ ξ K x = 0

Tactic:
funext k
-- 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 : α
h : 0 = (a *ᵥ ξ K x) k
⊢ (a *ᵥ ξ K x) k = 0

Tactic:
rw [eq_comm]

Premises used: eq_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 : α
u : K →+* ℂ
⊢ ξ K x ≠ 0

Tactic:
have hξ := ξ_ne_0 K x hxl
-- 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 : α
u : K →+* ℂ
hξ : ξ K x ≠ 0
⊢ ∃ (x_1 : β), ¬ξ K x x_1 = 0 x_1

Tactic:
rw [Ne, funext_iff, not_forall] at hξ

Premises used: funext_iff, Ne, Classical.not_forall
-- 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 : α
u : K →+* ℂ
hξ : ∃ (x_1 : β), ¬ξ K x x_1 = 0 x_1
rcases :
  ∀ (l : β) (hξ : ¬ξ K x l = 0 l),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0

Tactic:
rcases hξ with ⟨l, hξ⟩
-- 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 : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
rw :
  ∀ (hmulvec0 : ∀ (x_1 : Prod.{u_2, u_1} α (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1) (k : α) (u : K →+* ℂ) (l : β)
    (hξ : ¬ξ K x l = 0 l),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0

Tactic:
rw [funext_iff] at hmulvec0

Premises used: funext_iff
-- 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 : ∀ (x_1 : Prod.{u_2, u_1} α (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ (asiegel K a *ᵥ x) (k, u) = 0 (k, u)

Tactic:
specialize hmulvec0 ⟨k, u⟩

Premises used: Prod.mk
-- 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 β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : (asiegel K a *ᵥ x) (k, u) = 0 (k, u)
⊢ Eq (α := ℤ) (∑ x_1 : β, ∑ x_2 : K →+* ℂ, a' K a k x_1 x_2 u * x (x_1, x_2)) (0 (k, u))

Tactic:
simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0

Premises used: _private.0.NumberField.house.asiegel, dotProduct, Matrix.mulVec, Fintype.sum_prod_type
-- 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 β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : Eq (α := ℤ) (∑ x_1 : β, ∑ x_2 : K →+* ℂ, a' K a k x_1 x_2 u * x (x_1, x_2)) (0 (k, u))
⊢ Eq (α := ℤ) (∑ y : K →+* ℂ, ∑ x_1 : β, a' K a k x_1 y u * x (x_1, y)) (0 (k, u))

Tactic:
rw [sum_comm] at hmulvec0

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 β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : Eq (α := ℤ) (∑ y : K →+* ℂ, ∑ x_1 : β, a' K a k x_1 y u * x (x_1, y)) (0 (k, u))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0

Tactic:
mod_cast hmulvec0

Premises used: Int.cast, HMul.hMul, Finset.univ, congrArg, Int.cast_zero, cast, Prod.mk, Int.cast_sum._simp_1, Nat.cast, Int.cast_inj._simp_1, Int.cast_mul._simp_1, Eq.refl, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, _private.0.NumberField.house.a', Finset.sum_congr, Finset.sum, Eq.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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : Eq (α := ℤ) (∑ y : K →+* ℂ, ∑ x_1 : β, a' K a k x_1 y u * x (x_1, y)) (0 (k, u))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0

Tactic:
exact mod_cast hmulvec0
-- 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 : α
⊢ ∀ (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

Tactic:
have lin_0 : ∀ u, ∑ r, ∑ l, (a' K a k l r u * x (l, r) : 𝓞 K) = 0 := by
    intro u
    have hξ := ξ_ne_0 K x hxl
    rw [Ne, funext_iff, not_forall] at hξ
    rcases hξ with ⟨l, hξ⟩
    rw [funext_iff] at hmulvec0
    specialize hmulvec0 ⟨k, u⟩
    simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0
    rw [sum_comm] at hmulvec0
    exact mod_cast hmulvec0
-- 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
⊢ 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))

Tactic:
simp only [lin_0, zero_mul, sum_const_zero]

Premises used: MulZeroClass.zero_mul, Finset.sum_const_zero
-- 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
⊢ 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))

Tactic:
have : 0 = ∑ u, (∑ r, ∑ l, a' K a k l r u * x (l, r) : 𝓞 K) * (newBasis K) u := by
    simp only [lin_0, zero_mul, sum_const_zero]
-- 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))
h :
  ∀ (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
    (∑ 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))

Tactic:
enter [2, 2, u]
-- 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))
u : K →+* ℂ
h :
  ∑ i : K →+* ℂ,
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K) (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) 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)

Tactic:
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
    (∑ 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))
h :
  ∀ (u : K →+* ℂ),
    ∑ i : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)
| 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))

Tactic:
enter [2, 2, u]; 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
    (∑ 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
    (∑ u : K →+* ℂ,
      ∑ i : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))

Tactic:
conv at this => enter [2, 2, u]; 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
    (∑ u : K →+* ℂ,
      ∑ i : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
⊢ 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))

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

Tactic:
rw [sum_mul]

Premises used: Finset.sum_mul