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

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

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

Tactic:
rw [← lin_1]

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

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 : α
⊢ (a *ᵥ NumberField.house.ξ K x) k = 0 k

Tactic:
simp only [Pi.zero_apply]

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 : α
⊢ (a *ᵥ NumberField.house.ξ K x) k = 0

Proof state:
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

Tactic:
ext1 l

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

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

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

Tactic:
intros u

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