awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
hξ : ∃ (x_1 : β), ¬ξ K x x_1 = 0 x_1
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
have rcases : ∀ (l : β) (hξ : ¬ξ K x l = 0 l),
  Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
Tactic: rcases hξ with ⟨l, hξ⟩
Cleared hypotheses: hξ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
have rw : ∀ (hmulvec0 : ∀ (x_1 : Prod.{u_2, u_1} α (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1) (k : α) (u : K →+* ℂ) (l : β)
  (hξ : ¬ξ K x l = 0 l),
  Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
Tactic: rw [funext_iff] at hmulvec0
Cleared hypotheses: hmulvec0, k, u, l, hξ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : ∀ (x_1 : Prod.{u_2, u_1} α (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
have hmulvec0₁ : (asiegel K a *ᵥ x) (k, u) = 0 (k, u)
Tactic: specialize hmulvec0 ⟨k, u⟩
Cleared hypotheses: hmulvec0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : (asiegel K a *ᵥ x) (k, u) = 0 (k, u)
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
have hmulvec0₁ : Eq (α := ℤ) (∑ x_1 : β, ∑ x_2 : K →+* ℂ, a' K a k x_1 x_2 u * x (x_1, x_2)) (0 (k, u))
Tactic: simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0
Cleared hypotheses: hmulvec0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
hmulvec0 : Eq (α := ℤ) (∑ x_1 : β, ∑ x_2 : K →+* ℂ, a' K a k x_1 x_2 u * x (x_1, x_2)) (0 (k, u))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
have hmulvec0₁ : Eq (α := ℤ) (∑ y : K →+* ℂ, ∑ x_1 : β, a' K a k x_1 y u * x (x_1, y)) (0 (k, u))
Tactic: rw [sum_comm] at hmulvec0
Cleared hypotheses: hmulvec0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ 0 = (a *ᵥ ξ K x) k
have lin_0 : ∀ (u : K →+* ℂ),
  Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K)) 0
Tactic: have lin_0 : ∀ u, ∑ r, ∑ l, (a' K a k l r u * x (l, r) : 𝓞 K) = 0 := by
    intro u
    have hξ := ξ_ne_0 K x hxl
    rw [Ne, funext_iff, not_forall] at hξ
    rcases hξ with ⟨l, hξ⟩
    rw [funext_iff] at hmulvec0
    specialize hmulvec0 ⟨k, u⟩
    simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0
    rw [sum_comm] at hmulvec0
    exact mod_cast hmulvec0
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
⊢ 0 = (a *ᵥ ξ K x) k
have this : Eq.{u_1 + 1} (α := 𝓞 K) 0
  (∑ u : K →+* ℂ,
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
      (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
Tactic: have : 0 = ∑ u, (∑ r, ∑ l, a' K a k l r u * x (l, r) : 𝓞 K) * (newBasis K) u := by
    simp only [lin_0, zero_mul, sum_const_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
| Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
have h : ∀ (u : K →+* ℂ),
  HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
    (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)
Tactic: enter [2, 2, u]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
u : K →+* ℂ
| HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
    (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)
have h : ∑ i : K →+* ℂ,
  HMul.hMul (α := 𝓞 K) (β := 𝓞 K) (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)
Tactic: rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
| Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
have h : ∀ (u : K →+* ℂ),
  ∑ i : K →+* ℂ,
    HMul.hMul (α := 𝓞 K) (β := 𝓞 K) (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)
Tactic: enter [2, 2, u]; rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ r : K →+* ℂ,
      ∑ l : β,
        HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have this₁ : Eq.{u_1 + 1} (α := 𝓞 K) 0
  (∑ u : K →+* ℂ,
    ∑ i : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
Tactic: conv at this => enter [2, 2, u]; rw [sum_mul]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      ∑ i : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l i u) : 𝓞 K) (↑(x (l, i)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ r : K →+* ℂ,
      ∑ l : β,
        HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have this₁ : Eq.{u_1 + 1} (α := 𝓞 K) 0
  (∑ y : K →+* ℂ,
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
Tactic: rw [sum_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
⊢ Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ r : K →+* ℂ,
      ∑ l : β,
        HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have rw : Eq.{u_1 + 1} (α := 𝓞 K)
  (∑ y : K →+* ℂ,
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  (∑ r : K →+* ℂ,
    ∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ r : K →+* ℂ,
      ∑ l : β,
        HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have e_f : Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
  (fun (y : K →+* ℂ) ↦
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  fun (r : K →+* ℂ) ↦
  ∑ l : β,
    HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
⊢ Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
    (fun (y : K →+* ℂ) ↦
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    fun (r : K →+* ℂ) ↦
    ∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
have e_f : ∀ (r : K →+* ℂ),
  Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: ext1 r
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
| Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have h : ∀ (l : K →+* ℂ),
  HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
    (∑ l_1 : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l_1 r l) : 𝓞 K) (↑(x (l_1, r)) : 𝓞 K) : 𝓞 K)
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
Tactic: enter [1, 2, l]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r l : K →+* ℂ
| HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
    (∑ l_1 : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l_1 r l) : 𝓞 K) (↑(x (l_1, r)) : 𝓞 K) : 𝓞 K)
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
have h : ∑ i : β,
  HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
    ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
Tactic: rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
| Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have h : ∀ (l : K →+* ℂ),
  ∑ i : β,
    HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
      ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
Tactic: enter [1, 2, l]; rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ x_1 : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r x_1) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have e_f : Eq.{u_1 + 1} (α := 𝓞 K)
  (∑ l : K →+* ℂ,
    ∑ i : β,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K))
  (∑ l : β,
    HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: conv => enter [1, 2, l]; rw [sum_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : K →+* ℂ,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
          (∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l y x_1) : 𝓞 K) (↑(x (l, y)) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
r : K →+* ℂ
⊢ Eq.{u_1 + 1} (α := 𝓞 K)
    (∑ l : K →+* ℂ,
      ∑ i : β,
        HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k i r l) : 𝓞 K) (↑(x (i, r)) : 𝓞 K))
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K))
    (∑ l : β,
      HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
have e_f : Eq.{u_1 + 1} (α := 𝓞 K)
  (∑ y : β,
    ∑ x_1 : K →+* ℂ,
      HMul.hMul (β := 𝓞 K) (HMul.hMul (α := 𝓞 K) (↑(a' K a k y r x_1) : 𝓞 K) (↑(x (y, r)) : 𝓞 K))
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))
  (∑ l : β,
    HMul.hMul (α := 𝓞 K) (↑(x (l, r)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l r u) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
Tactic: rw [sum_comm]