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
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ LE.le (α := ℝ)
    (∑ j : K →+* ℂ,
      norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
    (∑ x : K →+* ℂ,
      (norm.{u_1} (E := (i j : K →+* ℂ) → ℂ) fun (i j : K →+* ℂ) ↦ (basisMatrix K)ᵀ⁻¹ i j) *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K))
have h : ∀ (j : K →+* ℂ),
  Membership.mem (γ := Finset (K →+* ℂ)) univ j →
    norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j) ≤
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
Tactic: gcongr with j
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
have _ : norm (E := ℂ)
    (↑(((((Basis.repr
                      (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                        (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                        (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                    K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                  (a : K) → (K →+* ℂ) →₀ ℚ)
                (↑α : K) :
              (K →+* ℂ) →₀ ℚ) :
            (a : K →+* ℂ) → ℚ)
          i) :
      ℂ) ≤
  ∑ j : K →+* ℂ,
    norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
      norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
Tactic: calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
_ :
  norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
⊢ norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
have _₁ : LE.le (α := ℝ)
  (∑ j : K →+* ℂ,
    norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
      norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
  (∑ j : K →+* ℂ,
    norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
      norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
Tactic: calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
_ :
  norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
_₁ :
  LE.le (α := ℝ)
    (∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
    (∑ j : K →+* ℂ,
      norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
⊢ norm (E := ℂ)
      (↑(((((Basis.repr
                        (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                          (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                          (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                      K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                    (a : K) → (K →+* ℂ) →₀ ℚ)
                  (↑α : K) :
                (K →+* ℂ) →₀ ℚ) :
              (a : K →+* ℂ) → ℚ)
            i) :
        ℂ) ≤
    c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
have _₂ : LE.le (α := ℝ)
  (∑ j : K →+* ℂ,
    norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
      norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j))
  (∑ x : K →+* ℂ,
    (norm.{u_1} (E := (i j : K →+* ℂ) → ℂ) fun (i j : K →+* ℂ) ↦ (basisMatrix K)ᵀ⁻¹ i j) *
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K))
Tactic: calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]
-- 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)
ha : a ≠ 0
⊢ ¬Eq (α := Matrix (Prod.{u_2, u_1} α (K →+* ℂ)) (Prod.{u_3, u_1} β (K →+* ℂ)) ℤ)
      (fun (k : Prod.{u_2, u_1} α (K →+* ℂ)) (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k.1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          k.2)
      0
have rw : ¬∀ (x : Prod.{u_2, u_1} α (K →+* ℂ)),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a x.1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          x.2)
      (0 x)
Tactic: rw [funext_iff]
-- 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)
ha : a ≠ 0
hs :
  ∀ (x : Prod.{u_2, u_1} α (K →+* ℂ)),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a x.1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          x.2)
      (0 x)
⊢ False
have hs₁ : ∀ (a_1 : α) (b : K →+* ℂ),
  Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
    (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
      (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a a_1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b)
    (0 (a_1, b))
Tactic: simp only [Prod.forall] at hs
Cleared hypotheses: hs
-- 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)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a a_1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (a_1, b))
⊢ False
have apply : a = 0
Tactic: apply ha
-- 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)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a a_1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (a_1, b))
⊢ a = 0
have rw : ∀ (i : α) (j : β), a i j = 0 i j
Tactic: rw [← Matrix.ext_iff]
-- 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)
ha : a ≠ 0
hs :
  ∀ (a_1 : α) (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a a_1 l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (a_1, b))
k' : α
l : β
⊢ a k' l = 0 k' l
have hs₁ : ∀ (b : K →+* ℂ),
  Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
    (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
      (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b)
    (0 (k', b))
Tactic: specialize hs k'
Cleared hypotheses: hs
-- 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)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (k', b))
⊢ a k' l = 0 k' l
have let : ∀ (b : K →+* ℂ), a k' l = 0 k' l
Tactic: let ⟨b⟩ := Fintype.card_pos_iff.1 (Fintype.card_pos (α := (K →+* ℂ)))
-- 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)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (k', b))
b : K →+* ℂ
⊢ Eq (α := (K →+* ℂ) →₀ ℤ)
    ((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
        (HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
      (K →+* ℂ) →₀ ℤ)
    (0 : (K →+* ℂ) →₀ ℤ)
have h : ∀ (b' : K →+* ℂ),
  Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    ((0 : (a : K →+* ℂ) → ℤ) b' : ℤ)
Tactic: ext b'
-- 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)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (k', b))
b b' : K →+* ℂ
⊢ Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    ((0 : (a : K →+* ℂ) → ℤ) b' : ℤ)
have hs₁ : Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
  (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
    (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
            (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
          (K →+* ℂ) →₀ ℤ) :
        (a : K →+* ℂ) → ℤ)
      b')
  (0 (k', b'))
Tactic: specialize hs b'
Cleared hypotheses: hs
-- 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)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs :
  Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
    (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
      (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b')
    (0 (k', b'))
⊢ Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    ((0 : (a : K →+* ℂ) → ℤ) b' : ℤ)
have hs₁ : ∀ (x : Prod.{u_3, u_1} β (K →+* ℂ)),
  Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' x.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x.2 : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    (0 (k', b') x : ℤ)
Tactic: rw [funext_iff] at hs
Cleared hypotheses: hs
-- 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)
ha : a ≠ 0
k' : α
l : β
b b' : K →+* ℂ
hs :
  ∀ (x : Prod.{u_3, u_1} β (K →+* ℂ)),
    Eq (α := ℤ)
      ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' x.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b' :
        ℤ)
      (0 (k', b') x : ℤ)
⊢ Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    ((0 : (a : K →+* ℂ) → ℤ) b' : ℤ)
have hs₁ : ∀ (a_1 : β) (b : K →+* ℂ),
  Eq (α := ℤ)
    ((((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
              (HMul.hMul (β := 𝓞 K) (a k' a_1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K)) :
            (K →+* ℂ) →₀ ℤ) :
          (a : K →+* ℂ) → ℤ)
        b' :
      ℤ)
    (0 (k', b') (a_1, b) : ℤ)
Tactic: simp only [Prod.forall] at hs
Cleared hypotheses: hs
-- 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)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (k', b))
b : K →+* ℂ
⊢ a k' l = 0 k' l
have this : HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) = 0
Tactic: have := ((newBasis K).repr.map_eq_zero_iff (x := (a k' l * (newBasis K) b))).1 <| by
    ext b'
    specialize hs b'
    rw [funext_iff] at hs
    simp only [Prod.forall] at hs
    apply hs
-- 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)
ha : a ≠ 0
k' : α
l : β
hs :
  ∀ (b : K →+* ℂ),
    Eq (α := (l : Prod.{u_3, u_1} β (K →+* ℂ)) → ℤ)
      (fun (l : Prod.{u_3, u_1} β (K →+* ℂ)) ↦
        (((Basis.repr (newBasis K) : (a : 𝓞 K) → (K →+* ℂ) →₀ ℤ)
                (HMul.hMul (β := 𝓞 K) (a k' l.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l.2 : 𝓞 K)) :
              (K →+* ℂ) →₀ ℤ) :
            (a : K →+* ℂ) → ℤ)
          b)
      (0 (k', b))
b : K →+* ℂ
this : HMul.hMul (β := 𝓞 K) (a k' l) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) = 0
⊢ a k' l = 0 k' l
have this₁ : a k' l = 0 ∨ Eq (α := 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) (0 : 𝓞 K)
Tactic: simp only [mul_eq_zero] 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_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
⊢ False
have apply : x = 0
Tactic: apply hxl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
⊢ x = 0
have h : ∀ (l : β) (r : K →+* ℂ), x (l, r) = 0 (l, r)
Tactic: ext ⟨l, 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_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)
have h : ∀ (H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1) (l : β) (r : K →+* ℂ), x (l, r) = 0 (l, r)
Tactic: rw [funext_iff] at H
Cleared hypotheses: H, l, r
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)
have hblin : LinearIndependent (ι := K →+* ℂ) ℤ (M := 𝓞 K) (⇑(newBasis K) : (a : K →+* ℂ) → 𝓞 K)
Tactic: have hblin := Basis.linearIndependent (newBasis K)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
β : Type u_3
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
hblin : LinearIndependent (ι := K →+* ℂ) ℤ (M := 𝓞 K) (⇑(newBasis K) : (a : K →+* ℂ) → 𝓞 K)
⊢ x (l, r) = 0 (l, r)
have hblin₁ : ∀ (g : (K →+* ℂ) → ℤ),
  Eq.{u_1 + 1} (α := 𝓞 K)
      (∑ x : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(g x) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x : 𝓞 K))
      0 →
    ∀ (i : K →+* ℂ), g i = 0
Tactic: simp only [zsmul_eq_mul, Fintype.linearIndependent_iff] at hblin
Cleared hypotheses: hblin
-- 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
⊢ a *ᵥ ξ K x = 0
have h : ∀ (k : α), (a *ᵥ ξ K x) k = 0 k
Tactic: funext k
-- 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 : α
⊢ (a *ᵥ ξ K x) k = 0
have h : 0 = (a *ᵥ ξ K x) k
Tactic: rw [eq_comm]
-- 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 : α
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
have hξ : ξ K x ≠ 0
Tactic: have hξ := ξ_ne_0 K x hxl
-- 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 : α
u : K →+* ℂ
hξ : ξ K x ≠ 0
⊢ 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 hξ₁ : ∃ (x_1 : β), ¬ξ K x x_1 = 0 x_1
Tactic: rw [Ne, funext_iff, not_forall] at hξ
Cleared hypotheses: hξ