awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
e_a :
  Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) → K)
    (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
    (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
      (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
      (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
⊢ Eq (α := ℚ)
    (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K)) (integralBasis K) :
              K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)| :
      ℚ)
    (|((Basis.det.{0, u_1, u_1} (R := ℚ) (M := K) (ι := Free.ChooseBasisIndex ℤ (𝓞 K))
                (Basis.localizationLocalization ℚ ℤ⁰ K (RingOfIntegers.basis K)) :
              K [⋀^Free.ChooseBasisIndex ℤ (𝓞 K)]→ₗ[ℚ] ℚ) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K) → K) → ℚ)
          (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
            (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
            (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
              (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))| :
      ℚ)

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
e_a :
  ∀ (x : Free.ChooseBasisIndex ℤ (𝓞 K)),
    Eq (α := K)
      (((Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
          x :
        K)
      (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
          (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
            (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
          x :
        K)
⊢ Eq (α := Free.ChooseBasisIndex ℤ (𝓞 K) → K)
    (⇑(Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
      (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
    (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
      (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
      (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
        (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.FractionalIdeal
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
I : (FractionalIdeal (R := 𝓞 K) (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)
x : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ Eq (α := K)
    (((Basis.reindex (basisOfFractionalIdeal K I) e.symm : Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℚ K) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → K)
        x :
      K)
    (Function.comp (β := ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        (Subtype.val (p := fun (x : K) ↦ x ∈ (↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K)))
        (⇑(Basis.reindex (fractionalIdealBasis K (↑I : FractionalIdeal (𝓞 K)⁰ K)) e.symm) :
          (a : Free.ChooseBasisIndex ℤ (𝓞 K)) → ↥(↑(↑I : FractionalIdeal (𝓞 K)⁰ K) : Submodule (𝓞 K) K))
        x :
      K)

Tactic:
simpa using basisOfFractionalIdeal_apply K I _

Premises used: NumberField.basisOfFractionalIdeal_apply
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
rw :
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) =
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
rw₁ :
  (↑(nnnorm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)) : ℝ) =
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
rw₂ :
  (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ) =
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
rw₃ rw₄ :
  (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ) =
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
⊢ house α = (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)

Tactic:
rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]

Premises used: Finset.univ_nonempty, NumberField.canonicalEmbedding.nnnorm_eq, coe_nnnorm, NumberField.house, Finset.sup'_eq_sup
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
simp :
  norm.{u_1} (E := (K →+* ℂ) → ℂ) (∑ x ∈ s, (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α x)) ≤
    ∑ x ∈ s, norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α x) : (K →+* ℂ) → ℂ)
⊢ house.{u_1} (K := K) (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)

Tactic:
simp only [house, map_sum]

Premises used: map_sum, NumberField.house
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
h :
  ∀ b ∈ s,
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ) ≤
      norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ)
⊢ norm.{u_1} (E := (K →+* ℂ) → ℂ) (∑ x ∈ s, (canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α x)) ≤
    ∑ x ∈ s, norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α x) : (K →+* ℂ) → ℂ)

Tactic:
apply norm_sum_le_of_le

Premises used: norm_sum_le_of_le
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ι : Type u_2
s : Finset ι
α : ι → K
b : ι
h : b ∈ s
⊢ norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ) ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
⊢ 0 ≤ house α

Tactic:
norm_nonneg _

Premises used: NumberField.house, norm_nonneg
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
simp :
  ‖HMul.hMul (α := (K →+* ℂ) → ℂ) (β := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)‖ ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) *
      norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)
⊢ house (α * β) ≤ house α * house β

Tactic:
simp only [house, map_mul]

Premises used: map_mul, NumberField.house
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
⊢ ‖HMul.hMul (α := (K →+* ℂ) → ℂ) (β := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)‖ ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) *
      norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)

Tactic:
apply norm_mul_le

Premises used: norm_mul_le
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Finset K
⊢ house (K := K) (∏ x ∈ s, x) ≤ ∏ x ∈ s, house x

Tactic:
simpa [house, map_prod] using Finset.norm_prod_le _ _

Premises used: map_prod, NumberField.house, Finset.norm_prod_le
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
simp :
  ‖HAdd.hAdd (α := (K →+* ℂ) → ℂ) (β := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)‖ ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) +
      norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)
⊢ house (α + β) ≤ house α + house β

Tactic:
simp only [house, map_add]

Premises used: map_add, NumberField.house
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
⊢ ‖HAdd.hAdd (α := (K →+* ℂ) → ℂ) (β := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)‖ ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) +
      norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) β : (K →+* ℂ) → ℂ)

Tactic:
apply norm_add_le

Premises used: norm_add_le
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
i : ℕ
⊢ house (α ^ i) ≤ house α ^ i

Tactic:
simpa only [house, map_pow] using norm_pow_le ((canonicalEmbedding K) α) i

Premises used: norm_pow_le, map_pow, NumberField.house, NumberField.canonicalEmbedding, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
c : ℕ
rw :
  (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) : ℝ) =
    (↑c : ℝ) * (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
⊢ house ((↑c : K) * α) = (↑c : ℝ) * house α

Tactic:
rw [house_eq_sup', house_eq_sup', Finset.sup'_eq_sup, Finset.sup'_eq_sup]

Premises used: Finset.sup'_eq_sup, NumberField.house_eq_sup'
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
c : ℕ
norm_cast :
  (sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) =
    HMul.hMul (α := NNReal) (↑c : NNReal) (sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ))
⊢ (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) : ℝ) =
    (↑c : ℝ) * (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
c : ℕ
⊢ (sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) =
    HMul.hMul (α := NNReal) (↑c : NNReal) (sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ))

Tactic:
simp [NNReal.mul_finset_sup]

Premises used: NNReal.mul_finset_sup
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ℤ
⊢ house.{u_1} (K := K) (↑x : K) = (↑|x| : ℝ)

Tactic:
simp only [house, map_intCast, Pi.intCast_def, pi_norm_const, Complex.norm_intCast, Int.cast_abs]

Premises used: Int.cast_abs, map_intCast, Pi.intCast_def, NumberField.house, pi_norm_const, Complex.norm_intCast
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
by_contra! : ∀ (h_neg : ∀ (w : InfinitePlace K), LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ) (1 : ℝ)), False
⊢ ∃ (w : InfinitePlace K), LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ)

Tactic:
by_contra! h_neg
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ) (1 : ℝ)
w₀ : InfinitePlace K := Classical.arbitrary (InfinitePlace K)
⊢ LE.le (α := ℝ) (1 : ℝ) ((w₀ : (a : K) → ℝ) (↑α : K) : ℝ)

Tactic:
have h_ge_one : 1 ≤ w₀ α := InfinitePlace.one_le_of_lt_one hα0 (fun z _ ↦ h_neg z)
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ) (1 : ℝ)
w₀ : InfinitePlace K := Classical.arbitrary (InfinitePlace K)
h_ge_one : LE.le (α := ℝ) (1 : ℝ) ((w₀ : (a : K) → ℝ) (↑α : K) : ℝ)
⊢ False

Tactic:
(h_neg w₀).not_ge h_ge_one

Premises used: LT.lt.not_ge
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ) (1 : ℝ)
w₀ : InfinitePlace K := Classical.arbitrary (InfinitePlace K)
h_ge_one : LE.le (α := ℝ) (1 : ℝ) ((w₀ : (a : K) → ℝ) (↑α : K) : ℝ)
⊢ False

Tactic:
exact (h_neg w₀).not_ge h_ge_one

Premises used: LT.lt.not_ge
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
obtain :
  ∀ (w : InfinitePlace K) (hw : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ)),
    ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) (↑α : K) : ℂ)
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) (↑α : K) : ℂ)

Tactic:
obtain ⟨w, hw⟩ : ∃ w : InfinitePlace K, 1 ≤ w α := by
    by_contra! h_neg
    let w₀ := Classical.arbitrary (InfinitePlace K)
    have h_ge_one : 1 ≤ w₀ α := InfinitePlace.one_le_of_lt_one hα0 (fun z _ ↦ h_neg z)
    exact (h_neg w₀).not_ge h_ge_one

Premises used: NumberField.InfinitePlace
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
w : InfinitePlace K
hw : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ)
h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑α : K) : ℂ)
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) (↑α : K) : ℂ)

Tactic:
use w.embedding

Premises used: NumberField.InfinitePlace.embedding
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
w : InfinitePlace K
hw h h₁ h₂ h₃ : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ)
⊢ 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑α : K) : ℂ)

Tactic:
rwa [InfinitePlace.norm_embedding_eq]

Premises used: NumberField.InfinitePlace.norm_embedding_eq
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
rw :
  norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
⊢ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤ house α

Tactic:
rw [house_eq_sup']

Premises used: NumberField.house_eq_sup'
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
⊢ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)

Tactic:
Finset.le_sup' (f := (‖· α‖₊)) (Finset.mem_univ σ)

Premises used: Finset.mem_univ, NNNorm.nnnorm, Finset.le_sup', NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
⊢ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤
    (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)

Tactic:
exact Finset.le_sup' (f := (‖· α‖₊)) (Finset.mem_univ σ)

Premises used: Finset.mem_univ, NNNorm.nnnorm, Finset.le_sup'
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
apply : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) α hα ≠ 0
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ)

Tactic:
apply exists_conjugate_one_le_norm (K := K) (α := ⟨α, hα⟩)

Premises used: NumberField.exists_conjugate_one_le_norm
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
⊢ Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) α hα ≠ 0

Tactic:
simpa [RingOfIntegers.ext_iff]

Premises used: NumberField.RingOfIntegers.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
have : ∀ (σ : K →+* ℂ) (hσ : 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ)), 1 ≤ house α
⊢ 1 ≤ house α

Tactic:
have ⟨σ, hσ⟩ : ∃ σ : K →+* ℂ, 1 ≤ ‖σ α‖ := by
    apply exists_conjugate_one_le_norm (K := K) (α := ⟨α, hα⟩)
    simpa [RingOfIntegers.ext_iff]
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
σ : K →+* ℂ
hσ : 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ)
⊢ 1 ≤ house α

Tactic:
apply hσ.trans (norm_embedding_le_house α σ)

Premises used: NumberField.norm_embedding_le_house, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)

Tactic:
?_
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
rw rw₁ : norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α) = norm (E := ℂ) (∏ x : K →ₐ[ℚ] ℂ, (x : (a : K) → ℂ) α)
⊢ norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α) =
    ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖

Tactic:
rw [mul_prod_erase univ (· α) (mem_univ σ')]

Premises used: Finset.mem_univ, Finset.univ, Finset.mul_prod_erase
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖ ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)

Tactic:
?_
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
hbc : ∀ i ∈ erase univ σ', norm (E := ℂ) ((i : (a : K) → ℂ) α : ℂ) ≤ house α
⊢ norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ) ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', house α

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
i : K →ₐ[ℚ] ℂ
h : i ∈ erase univ σ'
⊢ norm (E := ℂ) ((i : (a : K) → ℂ) α : ℂ) ≤ house α

Tactic:
apply norm_embedding_le_house

Premises used: NumberField.norm_embedding_le_house
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', house α =
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
calc_1 : norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
calc_2 :
  ‖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:
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

Premises used: Finset.univ, Rat, HSub.hSub, NumberField.house, OfNat.ofNat, Finset.erase, DFunLike.coe, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
calc_1 :
  norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
calc_1₁ :
  norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
calc_1₂ :
  |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
calc_1₃ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℂ)
calc_1₄ calc_1₅ : Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)|
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)

Tactic:
rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]

Premises used: Algebra.norm_eq_prod_embeddings, Complex.norm_ratCast, Rat.norm_cast_real, eq_ratCast, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
calc_2 :
  norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
⊢ ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖ ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)

Tactic:
rw [Complex.norm_mul]

Premises used: Complex.norm_mul
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
calc_2 :
  norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
    ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
⊢ norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)

Tactic:
gcongr
-- 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:
norm_prod_le (univ.erase σ') (· α)

Premises used: Finset.univ, Finset.erase, Finset.norm_prod_le, DFunLike.coe