awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.FractionalIdeal (goal)
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)
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
⊢ house α = (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
have rw : norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ) =
  (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α : ℂ)) : ℝ)
⊢ house α = (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
have rw₁ : (↑(nnnorm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) α : (K →+* ℂ) → ℂ)) : ℝ) =
  (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α : ℂ)) : ℝ)
⊢ house α = (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
have rw₂ : (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ) =
  (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α : ℂ)) : ℝ)
⊢ house α = (↑(sup' univ ⋯ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
have rw₃ : (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ) =
  (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]
-- 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
s : Finset ι
α : ι → K
⊢ house.{u_1} (K := K) (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)
have 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 →+* ℂ) → ℂ)
Tactic: simp only [house, map_sum]
-- 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
s : Finset ι
α : ι → 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 →+* ℂ) → ℂ)
have h : ∀ b ∈ s,
  norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ) ≤
    norm (E := (K →+* ℂ) → ℂ) ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) (α b) : (K →+* ℂ) → ℂ)
Tactic: apply norm_sum_le_of_le
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
⊢ house (α * β) ≤ house α * house β
have 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 →+* ℂ) → ℂ)
Tactic: simp only [house, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α β : K
⊢ house (α + β) ≤ house α + house β
have 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 →+* ℂ) → ℂ)
Tactic: simp only [house, map_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
c : ℕ
⊢ house ((↑c : K) * α) = (↑c : ℝ) * house α
have rw : (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) : ℝ) =
  (↑c : ℝ) * (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house_eq_sup', house_eq_sup', Finset.sup'_eq_sup, Finset.sup'_eq_sup]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
c : ℕ
⊢ (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) ((↑c : K) * α) : ℂ)) : ℝ) =
    (↑c : ℝ) * (↑(sup univ fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
have 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) → ℂ) α : ℂ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
⊢ ∃ (w : InfinitePlace K), LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ)
have by_contra! : ∀ (h_neg : ∀ (w : InfinitePlace K), LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑α : K) : ℝ) (1 : ℝ)), False
Tactic: by_contra! h_neg
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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)
⊢ False
have h_ge_one : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) (↑α : K) : ℂ)
have obtain : ∀ (w : InfinitePlace K) (hw : LE.le (α := ℝ) (1 : ℝ) ((w : (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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) : ℝ)
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) (↑α : K) : ℂ)
have h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑α : K) : ℂ)
Tactic: use w.embedding
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
⊢ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤ house α
have rw : norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) ≤
  (↑(sup' univ sorry fun (φ : K →+* ℂ) ↦ nnnorm (E := ℂ) ((φ : (a : K) → ℂ) α : ℂ)) : ℝ)
Tactic: rw [house_eq_sup']
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
⊢ ∃ (σ : K →+* ℂ), 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ)
have apply : Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) α hα ≠ 0
Tactic: apply exists_conjugate_one_le_norm (K := K) (α := ⟨α, hα⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
hα : IsIntegral ℤ α
hα0 : α ≠ 0
⊢ 1 ≤ house α
have have : ∀ (σ : K →+* ℂ) (hσ : 1 ≤ norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ)), 1 ≤ house α
Tactic: have ⟨σ, hσ⟩ : ∃ σ : K →+* ℂ, 1 ≤ ‖σ α‖ := by
    apply exists_conjugate_one_le_norm (K := K) (α := ⟨α, hα⟩)
    simpa [RingOfIntegers.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α) =
    ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖
have rw : norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α) = norm (E := ℂ) (∏ x : K →ₐ[ℚ] ℂ, (x : (a : K) → ℂ) α)
Tactic: rw [mul_prod_erase univ (· α) (mem_univ σ')]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ) ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', house α
have hbc : ∀ i ∈ erase univ σ', norm (E := ℂ) ((i : (a : K) → ℂ) α : ℂ) ≤ house α
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)
have calc_1 : norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)
have calc_2 : ‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖ ≤
  norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α)
have calc_1 : norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) =
  norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
Tactic: rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℚ) α : ℚ) : ℂ)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
have calc_1₁ : norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ) =
  norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
Tactic: rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℚ) α : ℚ) : ℂ)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
have calc_1₂ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| =
  norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) : ℂ)
Tactic: rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℚ) α : ℚ) : ℂ)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
have calc_1₃ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℂ)
Tactic: rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℚ) α) : ℂ)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
have calc_1₄ : Eq (α := ℝ) |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)| |(↑((Algebra.norm ℚ : (a : K) → ℚ) α) : ℝ)|
Tactic: rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α : ℂ)
have calc_2 : norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
  norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
Tactic: rw [Complex.norm_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤
    norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
have calc_2 : norm (E := ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α) ≤ ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)
have calc_1 : norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) = norm (E := ℂ) (∏ τ : K →ₐ[ℚ] ℂ, (τ : (a : K) → ℂ) α)
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 σ') (· α)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) → ℂ) α)
⊢ norm (E := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) α : ℚ) ≤
    norm (E := ℂ) ((σ : (a : K) → ℂ) α : ℂ) * house α ^ (finrank ℚ K - 1)
have calc_2 : let σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom;
‖HMul.hMul (α := ℂ) (β := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) (∏ τ ∈ erase univ σ', (τ : (a : K) → ℂ) α : ℂ)‖ ≤
  norm (E := ℂ) ((σ' : (a : K) → ℂ) α : ℂ) * ∏ τ ∈ erase univ σ', norm (E := ℂ) ((τ : (a : K) → ℂ) α : ℂ)
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 σ') (· α)
-- 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)
have 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)
Tactic: rw [← inverse_basisMatrix_mulVec_eq_repr]
-- 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 := ℂ) ((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))
have 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)ᵀ⁻¹
Tactic: gcongr