awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
    ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)

Tactic:
exact norm_prod_le (univ.erase σ') (· α)

Premises used: Finset.univ, Finset.erase, Finset.norm_prod_le, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
set set₁ :
  norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)
calc_1 : norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
calc_2 calc_2₁ :
  let σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom;
  ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖ ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)

Tactic:
classical
  set σ' := σ.toRatAlgHom
  calc _ = ‖∏ τ : K →ₐ[ℚ] ℂ, τ α‖ := ?_
       _ = ‖(σ' α) * ∏ τ ∈ univ.erase σ', τ α‖ := by rw [mul_prod_erase univ (· α) (mem_univ σ')]
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖ := ?_
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', house α := by gcongr; apply norm_embedding_le_house
       _ = ‖σ' α‖ * house α ^ (Module.finrank ℚ K - 1) := by simp
  · rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
  · rw [Complex.norm_mul]
    gcongr
    exact norm_prod_le (univ.erase σ') (· α)

Premises used: Rat, Algebra.norm_eq_prod_embeddings, HSub.hSub, RingHom.toRatAlgHom, Complex.norm_ratCast, Rat.norm_cast_real, NumberField.house, eq_ratCast, OfNat.ofNat, Complex.norm_mul, Module.finrank, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ 0 ≤ (↑(finrank ℚ K) : ℝ) * norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
rw :
  ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun (j : K →+* ℂ) ↦
          (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
        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) :
        ℂ) ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)

Tactic:
rw [← inverse_basisMatrix_mulVec_eq_repr]

Premises used: NumberField.inverse_basisMatrix_mulVec_eq_repr
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun (j : K →+* ℂ) ↦
          (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
        i‖ ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)

Tactic:
norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le

Premises used: Algebra.algebraMap, dotProduct, Eq.le, norm_sum_le_of_le, norm_mul, Inv.inv, Matrix.transpose, NumberField.canonicalEmbedding, NumberField.RingOfIntegers, Matrix.mulVec, DFunLike.coe, NumberField.basisMatrix
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖((basisMatrix K)ᵀ⁻¹ *ᵥ fun (j : K →+* ℂ) ↦
          (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)
        i‖ ≤
    ∑ j : K →+* ℂ,
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i j) *
        norm (E := ℂ) ((σ : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K) j)

Tactic:
exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le

Premises used: Eq.le, norm_sum_le_of_le, norm_mul
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
h :
  ∀ (i_1 : K →+* ℂ),
    Membership.mem (γ := Finset (K →+* ℂ)) univ i_1 →
      norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i i_1) ≤ norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹
⊢ 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:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
i_1 : K →+* ℂ
h : Membership.mem (γ := Finset (K →+* ℂ)) univ i_1
⊢ norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i i_1) ≤ norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹

Tactic:
norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹

Premises used: Matrix.norm_entry_le_entrywise_sup_norm, Inv.inv, Matrix.transpose, NumberField.basisMatrix
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
i_1 : K →+* ℂ
h : Membership.mem (γ := Finset (K →+* ℂ)) univ i_1
⊢ norm (E := ℂ) ((basisMatrix K)ᵀ⁻¹ i i_1) ≤ norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹

Tactic:
exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹

Premises used: Matrix.norm_entry_le_entrywise_sup_norm, Inv.inv, Matrix.transpose, NumberField.basisMatrix
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
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)
⊢ 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:
gcongr with j
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
h : 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:
norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j

Premises used: Algebra.algebraMap, norm_le_pi_norm, NumberField.house, NumberField.RingOfIntegers, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
j : K →+* ℂ
h : 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:
exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j

Premises used: Algebra.algebraMap, norm_le_pi_norm, NumberField.RingOfIntegers, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ 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) =
    (↑(finrank ℚ K) : ℝ) * norm (E := Matrix (K →+* ℂ) (K →+* ℂ) ℂ) (basisMatrix K)ᵀ⁻¹ *
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)

Tactic:
simp [Embeddings.card, mul_assoc]

Premises used: mul_assoc, NumberField.Embeddings.card
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 ≤ supOfBasis K

Tactic:
simp only [supOfBasis, le_sup'_iff, mem_univ, and_self,
    exists_const, house_nonneg]

Premises used: Finset.mem_univ, Finset.le_sup'_iff, and_self, _private.0.NumberField.house.supOfBasis, NumberField.house_nonneg, exists_const
-- Module: Mathlib.NumberTheory.NumberField.House
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
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)
⊢ ¬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

Tactic:
rw [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.NumberTheory.NumberField.House
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)
⊢ ∀ (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

Premises used: Prod.forall
-- Module: Mathlib.NumberTheory.NumberField.House
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))
apply : a = 0
⊢ False

Tactic:
apply ha
-- Module: Mathlib.NumberTheory.NumberField.House
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))
rw : ∀ (i : α) (j : β), a i j = 0 i j
⊢ a = 0

Tactic:
rw [← Matrix.ext_iff]

Premises used: Matrix.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.House
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 : β
⊢ ∀ (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'
-- Module: Mathlib.NumberTheory.NumberField.House
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))
let : ∀ (b : K →+* ℂ), a k' l = 0 k' l
⊢ a k' l = 0 k' l

Tactic:
let ⟨b⟩ := Fintype.card_pos_iff.1 (Fintype.card_pos (α := (K →+* ℂ)))
-- Module: Mathlib.NumberTheory.NumberField.House
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 →+* ℂ
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' : ℤ)
⊢ 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 →+* ℂ) →₀ ℤ)

Tactic:
ext b'
-- Module: Mathlib.NumberTheory.NumberField.House
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 (α := (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'
-- Module: Mathlib.NumberTheory.NumberField.House
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'))
⊢ ∀ (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

Premises used: funext_iff
-- Module: Mathlib.NumberTheory.NumberField.House
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 : ℤ)
⊢ ∀ (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

Premises used: Prod.forall
-- Module: Mathlib.NumberTheory.NumberField.House
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 :
  ∀ (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) : ℤ)
⊢ 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:
apply hs
-- Module: Mathlib.NumberTheory.NumberField.House
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 →+* ℂ
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.House
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 ∨ Eq (α := 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) (0 : 𝓞 K)

Tactic:
simp only [mul_eq_zero] at this

Premises used: mul_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.House
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 : a k' l = 0 ∨ Eq (α := 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) (0 : 𝓞 K)
⊢ a k' l = 0 k' l

Tactic:
this.resolve_right (Basis.ne_zero (newBasis K) b)

Premises used: _private.0.NumberField.house.newBasis, Module.Basis.ne_zero, Or.resolve_right
-- Module: Mathlib.NumberTheory.NumberField.House
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 : a k' l = 0 ∨ Eq (α := 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) (0 : 𝓞 K)
⊢ a k' l = 0 k' l

Tactic:
exact this.resolve_right (Basis.ne_zero (newBasis K) b)

Premises used: _private.0.NumberField.house.newBasis, Module.Basis.ne_zero, Or.resolve_right
-- Module: Mathlib.NumberTheory.NumberField.House
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
apply : x = 0
⊢ False

Tactic:
apply hxl
-- Module: Mathlib.NumberTheory.NumberField.House
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
h : ∀ (l : β) (r : K →+* ℂ), x (l, r) = 0 (l, r)
⊢ x = 0

Tactic:
ext ⟨l, r⟩
-- Module: Mathlib.NumberTheory.NumberField.House
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 →+* ℂ
h : ∀ (H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1) (l : β) (r : K →+* ℂ), x (l, r) = 0 (l, r)
⊢ x (l, r) = 0 (l, r)

Tactic:
rw [funext_iff] at H

Premises used: funext_iff