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

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

Tactic:
funext k

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 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 β
hmulvec0 : ∀ (x_1 : α × (K →+* ℂ)), (NumberField.house.asiegel K a *ᵥ x) x_1 = 0 x_1
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

Tactic:
specialize hmulvec0 ⟨k, u⟩

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 : (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

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 →+* ℂ,
      (∑ r : K →+* ℂ, ∑ l : β, ↑(NumberField.house.a' K a k l r u) * ↑(x (l, r))) * (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:
conv at this => enter [2, 2, u]; rw [sum_mul]

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

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

Tactic:
rw [sum_comm] 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 : ∑ 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

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

Tactic:
congr 1

Result:
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

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

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

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 →+* ℂ
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

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

Tactic:
ring

Result:
no goals

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

Tactic:
rw [eq_comm]

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

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:
have hξ := ξ_ne_0 K x hxl

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