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

Proof state:
case e_f.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 =
    ∑ 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
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1 : K →+* ℂ, ↑(NumberField.house.a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (NumberField.house.newBasis K) x_1 =
    ∑ i : K →+* ℂ, ↑(x (r, r✝)) * (↑(NumberField.house.a' K a k r r✝ i) * (NumberField.house.newBasis K) i)

Tactic:
congr 1

Result:
case e_f.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 =
    ∑ 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
r✝ : K →+* ℂ
r : β
⊢ (fun x_1 => ↑(NumberField.house.a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (NumberField.house.newBasis K) x_1) = fun i =>
    ↑(x (r, r✝)) * (↑(NumberField.house.a' K a k r r✝ i) * (NumberField.house.newBasis K) i)

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
⊢ ∑ 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

Tactic:
congr 1

Result:
case 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
⊢ (fun 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) =
    fun i => (fun j => a k j) i * NumberField.house.ξ K x i

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 : (NumberField.house.asiegel K a *ᵥ x) (k, u) = 0 (k, u)
⊢ ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0

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

Result:
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 : ∑ x_1 : β, ∑ x_2 : K →+* ℂ, NumberField.house.a' K a k x_1 x_2 u * x (x_1, x_2) = 0 (k, u)
⊢ ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0

Proof state:
case 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 =
    ∑ 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
⊢ (fun y =>
      ∑ x_1 : K →+* ℂ,
        (∑ l : β, ↑(NumberField.house.a' K a k l y x_1) * ↑(x (l, y))) * (NumberField.house.newBasis K) x_1) =
    fun r =>
    ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u

Tactic:
ext1 r

Result:
case 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 =
    ∑ 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
r : K →+* ℂ
⊢ ∑ x_1 : K →+* ℂ, (∑ l : β, ↑(NumberField.house.a' K a k l r x_1) * ↑(x (l, r))) * (NumberField.house.newBasis K) x_1 =
    ∑ l : β, ↑(x (l, r)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k l r u) * (NumberField.house.newBasis K) u

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 : α
u : K →+* ℂ
hξ : ∃ x_1, ¬NumberField.house.ξ K x x_1 = 0 x_1
⊢ ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
rcases hξ with ⟨l, hξ⟩

Result:
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 β
hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
l : β
hξ : ¬NumberField.house.ξ K x l = 0 l
⊢ ∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r)) = 0

Proof state:
case e_f.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 =
    ∑ 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
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1 : K →+* ℂ, ↑(NumberField.house.a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (NumberField.house.newBasis K) x_1 =
    ↑(x (r, r✝)) * ∑ u : K →+* ℂ, ↑(NumberField.house.a' K a k r r✝ u) * (NumberField.house.newBasis K) u

Tactic:
rw [mul_sum]

Result:
case e_f.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 =
    ∑ 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
r✝ : K →+* ℂ
r : β
⊢ ∑ x_1 : K →+* ℂ, ↑(NumberField.house.a' K a k r r✝ x_1) * ↑(x (r, r✝)) * (NumberField.house.newBasis K) x_1 =
    ∑ i : K →+* ℂ, ↑(x (r, r✝)) * (↑(NumberField.house.a' K a k r r✝ i) * (NumberField.house.newBasis K) i)