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

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

Tactic:
rw [sum_comm]

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

Tactic:
ring

Result:
no goals

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

Tactic:
congr 1

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

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

Tactic:
conv => enter [1, 2, l]; rw [sum_mul]

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

Tactic:
simp only [lin_0, zero_mul, sum_const_zero]

Result:
no goals

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

Tactic:
ext1 r

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