awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : { φ : K →+* ℂ // ¬ComplexEmbedding.IsReal φ }
⊢ (↑(mkComplex φ) : InfinitePlace K) = mk (↑φ : K →+* ℂ)

Tactic:
rfl

Premises used: NumberField.InfinitePlace.mk, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)

Tactic:
(congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm

Premises used: Norm.norm, Rat, Algebra.norm_eq_prod_embeddings, congr_arg, Complex, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
h₁ :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)

Tactic:
convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm

Premises used: Norm.norm, Rat, Algebra.norm_eq_prod_embeddings, congr_arg, Complex, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
x_1 : K →+* ℂ
⊢ Eq (α := ℝ) ((fun (f : K →+* ℂ) ↦ norm (E := ℂ) ((f : (a : K) → ℂ) x : ℂ)) x_1)
    ((fun (φ : K →ₐ[ℚ] ℂ) ↦ norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ))
      ((RingHom.equivRatAlgHom : (a : K →+* ℂ) → K →ₐ[ℚ] ℂ) x_1))

Tactic:
simp [RingHom.equivRatAlgHom_apply]

Premises used: RingHom.equivRatAlgHom_apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : K →+* ℂ, norm (E := ℂ) ((x_1 : (a : K) → ℂ) x : ℂ))
⊢ ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)

Tactic:
rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]

Premises used: Norm.norm, Fintype.prod_equiv, norm_prod, DFunLike.coe, RingHom.equivRatAlgHom
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : K →+* ℂ, norm (E := ℂ) ((x_1 : (a : K) → ℂ) x : ℂ))

Tactic:
rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]

Premises used: Norm.norm, Finset.univ, NumberField.InfinitePlace.mk, Finset.prod_fiberwise, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
w : InfinitePlace K
φ : K →+* ℂ
hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ
rw : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
rw₁ rw₂ : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x

Tactic:
rw [← (Finset.mem_filter.mp hφ).2, apply]

Premises used: And.right, Iff.mp, Finset.mem_filter, NumberField.InfinitePlace.apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ ∀ (w : InfinitePlace K) (φ : K →+* ℂ) (hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x

Tactic:
have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
this :
  ∀ (w : InfinitePlace K) (φ : K →+* ℂ) (hφ : Membership.mem (γ := Finset (K →+* ℂ)) {φ : K →+* ℂ | mk φ = w} φ),
    norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
h :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : InfinitePlace K, ∏ x_2 : K →+* ℂ with mk x_2 = x_1, (x_1 : (a : K) → ℝ) x)
h₁ :
  Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ x_1 : InfinitePlace K,
      HPow.hPow (α := ℝ) ((x_1 : (a : K) → ℝ) x : ℝ) (Finset.card.{u_1} (α := K →+* ℂ) {i : K →+* ℂ | mk i = x_1}))
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (∏ j : InfinitePlace K, ∏ i : K →+* ℂ with mk i = j, norm (E := ℂ) ((i : (a : K) → ℂ) x : ℂ))

Tactic:
simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]

Premises used: NumberField.InfinitePlace.card_filter_mk_eq, Finset.prod_congr, Finset.prod_const, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h : (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₁ : |(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ)| = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₂ : norm (E := ℝ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₃ : ‖(↑(↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℝ) : ℂ)‖ = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
h₄ h₅ :
  norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ) = norm (E := ℂ) (↑((Algebra.norm ℚ : (a : K) → ℚ) x) : ℂ)
⊢ (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)

Tactic:
rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]

Premises used: Complex.norm_real, Rat.cast_abs, eq_ratCast, Complex.ofReal_ratCast, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h :
  ∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult =
    norm (E := ℂ) (∏ σ : K →ₐ[ℚ] ℂ, (σ : (a : K) → ℂ) x)
h₁ h₂ :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ) =
    norm (E := ℂ) ((algebraMap ℚ ℂ : (a : ℚ) → ℂ) ((Algebra.norm ℚ : (a : K) → ℚ) x : ℚ) : ℂ)
⊢ Eq (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)

Tactic:
classical
  convert! (congr_arg (‖·‖) (Algebra.norm_eq_prod_embeddings ℚ ℂ x)).symm
  · rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
    rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
    have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
    simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
  · rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]

Premises used: Norm.norm, Fintype.prod_equiv, Rat, Algebra.norm_eq_prod_embeddings, NumberField.InfinitePlace.card_filter_mk_eq, Complex.norm_real, Finset.prod_const, congr_arg, norm_prod, Rat.cast_abs, eq_ratCast, Complex.ofReal_ratCast, Complex, Eq.symm, DFunLike.coe, RingHom.equivRatAlgHom, Real.norm_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ)
contrapose! :
  ∀ (this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)),
    LT.lt (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) 1
⊢ LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ)

Tactic:
contrapose! this
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
rw :
  LT.lt (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) w.mult)
    (∏ _x : InfinitePlace K, 1)
rw₁ : Type u_1
rw₂ : Finset (InfinitePlace K)
⊢ LT.lt (α := ℝ) (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ) 1

Tactic:
rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]

Premises used: Finset.prod_const_one, NumberField.InfinitePlace.prod_eq_abs_norm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) w.mult)
    (∏ _x : InfinitePlace K, 1)

Tactic:
Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty

Premises used: Finset.univ_nonempty, Finset.prod_lt_prod_of_nonempty
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
x : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
⊢ 0 < HPow.hPow (α := ℝ) ((x : (a : K) → ℝ) (↑a : K) : ℝ) x.mult

Tactic:
pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _

Premises used: Iff.mpr, pow_pos, NumberField.InfinitePlace.pos_iff, Iff.not, Subalgebra.coe_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
x : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ x
⊢ 0 < HPow.hPow (α := ℝ) ((x : (a : K) → ℝ) (↑a : K) : ℝ) x.mult

Tactic:
exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _

Premises used: Iff.mpr, pow_pos, NumberField.InfinitePlace.pos_iff, Iff.not, Subalgebra.coe_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
pos : z.IsReal → Ne (α := ℕ) 1 0
neg : ¬z.IsReal → Ne (α := ℕ) 2 0
⊢ Ne (α := ℕ) (if z.IsReal then 1 else 2) 0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
h_2 : z.IsReal
⊢ Ne (α := ℕ) 1 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
h_2 : ¬z.IsReal
⊢ Ne (α := ℕ) 2 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
refine_2 : LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ HPow.hPow (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) z.mult < 1

Tactic:
refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)

Premises used: pow_lt_one₀, NonnegHomClass.apply_nonneg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
pos : ∀ (hz : z = w), LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
neg : ∀ (hz : ¬z = w), LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)

Tactic:
by_cases hz : z = w
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
hz : z = w
pos pos₁ pos₂ pos₃ : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)

Tactic:
rwa [hz]
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
hz : ¬z = w
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)

Tactic:
h hz
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
this : LT.lt (α := ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
z : InfinitePlace K
h_1 : Membership.mem (γ := Finset (InfinitePlace K)) Finset.univ z
hz : ¬z = w
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)

Tactic:
exact h hz
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
suffices : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ)
⊢ LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ)

Tactic:
suffices (1 : ℝ) ≤ |Algebra.norm ℚ (a : K)| by
    contrapose! this
    rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
    refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
    · exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _
    · refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
      by_cases hz : z = w
      · rwa [hz]
      · exact h hz
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
rw : LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a| : ℤ)
⊢ LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)| : ℝ)

Tactic:
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]

Premises used: Int.cast_abs, Rat.cast_intCast, Int.cast_le, Algebra.coe_norm_int, Int.cast_one
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a| : ℤ)

Tactic:
Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr ha)

Premises used: Iff.mpr, Int.one_le_abs, Algebra.norm_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
⊢ LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a| : ℤ)

Tactic:
exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr ha)

Premises used: Iff.mpr, Int.one_le_abs, Algebra.norm_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
rw :
  ∀ (ψ : K →ₐ[ℚ] ℂ),
    Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) →
      w.embedding.toRatAlgHom = ψ
rw₁ : ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits
⊢ Eq (α := IntermediateField ℚ K) ℚ⟮(↑x : K)⟯ ⊤

Tactic:
rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom]

Premises used: Rat, RingHom.toRatAlgHom, NumberField.InfinitePlace.embedding, Complex, Field.primitive_element_iff_algHom_eq_of_eval
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)

Tactic:
have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
⊢ 1 ≤ norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)

Tactic:
rw [← norm_embedding_eq, hψ] at h

Premises used: NumberField.InfinitePlace.norm_embedding_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : 1 ≤ norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
contrapose! : ∀ (h : w ≠ mk ψ.toRingHom), norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) < 1
⊢ w = mk ψ.toRingHom

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : w ≠ mk ψ.toRingHom
⊢ norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) < 1

Tactic:
h₂ h.symm

Premises used: Ne.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : w ≠ mk ψ.toRingHom
⊢ norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) < 1

Tactic:
exact h₂ h.symm

Premises used: Ne.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
⊢ w = mk ψ.toRingHom

Tactic:
have main : w = InfinitePlace.mk ψ.toRingHom := by
      simp only [RingHom.toRatAlgHom_apply] at hψ
      rw [← norm_embedding_eq, hψ] at h
      contrapose! h
      exact h₂ h.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
h₃ : w.IsReal ∨ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w = mk ψ.toRingHom
⊢ w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom

Tactic:
rw [(mk_embedding w).symm, mk_eq_iff] at main

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → LT.lt (α := ℝ) ((w' : (a : K) → ℝ) (↑x : K) : ℝ) (1 : ℝ)
ψ : K →ₐ[ℚ] ℂ
hψ : Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : w.IsReal
⊢ w.embedding = ψ.toRingHom

Tactic:
rw [conjugate_embedding_eq_of_isReal hw, or_self] at main

Premises used: NumberField.InfinitePlace.conjugate_embedding_eq_of_isReal, or_self