-- Mathlib/NumberTheory/NumberField/House.lean
theorem ξ_mulVec_eq_0 : a *ᵥ ξ K x = 0

Proof state:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
⊢ 0 = (a *ᵥ NumberField.house.ξ K x) 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

Result:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this✝ :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
this :
  0 =
    ∑ r : K →+* ℂ,
      ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u
⊢ 0 = (a *ᵥ NumberField.house.ξ K x) k

Proof state:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this✝ :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
this :
  0 =
    ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u
⊢ 0 = (a *ᵥ NumberField.house.ξ K x) k

Tactic:
rw [this]

Result:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this✝ :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
this :
  0 =
    ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u
⊢ ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u =
    (a *ᵥ NumberField.house.ξ K x) k

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬NumberField.house.ξ K x l = 0 l
hmulvec0 : ∑ y : K →+* ℂ, ∑ x_1 : β, NumberField.house.a' K a k x_1 y u * x (x_1, y) = 0 (k, u)
⊢ ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
exact mod_cast hmulvec0

Result:
no goals

Proof state:
case h.e_f.h
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this✝ :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
this :
  0 =
    ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u
l : β
⊢ ∑ x_1 : K →+* ℂ,
      ↑(x (l, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l x_1 u) * (NumberField.house.newBasis K) u =
    ∑ i : K →+* ℂ, (fun j => a k j) l * (↑(x (l, i)) * (NumberField.house.newBasis K) i)

Tactic:
congr 1

Result:
case h.e_f.h.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this✝ :
  0 =
    ∑ u : K →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (NumberField.house.newBasis K) u
this :
  0 =
    ∑ y : β,
      ∑ x_1 : K →+* ℂ,
        ↑(x (y, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k y x_1 u) * (NumberField.house.newBasis K) u
l : β
⊢ (fun x_1 => ↑(x (l, x_1)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l x_1 u) * (NumberField.house.newBasis K) u) =
    fun i => (fun j => a k j) l * (↑(x (l, i)) * (NumberField.house.newBasis K) i)

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this :
  0 =
    ∑ u : K →+* ℂ,
      ∑ i : K →+* ℂ, (∑ l : β, ↑(NumberField.house.a' K a k l i u) * ↑(x (l, i))) * (NumberField.house.newBasis K) u
⊢ 0 =
    ∑ r : K →+* ℂ,
      ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u

Tactic:
rw [sum_comm] at this

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0
this :
  0 =
    ∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        (∑ l : β, ↑(NumberField.house.a' K a k l y x_1) * ↑(x (l, y))) * (NumberField.house.newBasis K) x_1
⊢ 0 =
    ∑ r : K →+* ℂ,
      ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u