awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : ℝ)
⊢ LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
have neg : ∀ (hz : ¬z = w), LT.lt (α := ℝ) ((z : (a : K) → ℝ) (↑a : K) : ℝ) (1 : ℝ)
Tactic: by_cases hz : z = w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : ℝ) ((w : (a : K) → ℝ) (↑a : K) : ℝ)
have suffices : LE.le (α := ℝ) 1 (↑|(Algebra.norm ℚ : (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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : K)| : ℝ)
have rw : LE.le (α := ℤ) (1 : ℤ) (|(Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a| : ℤ)
Tactic: rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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
⊢ Eq (α := IntermediateField ℚ K) ℚ⟮(↑x : K)⟯ ⊤
have rw : ∀ (ψ : K →ₐ[ℚ] ℂ),
  Eq (α := ℂ) ((w.embedding.toRatAlgHom : (a : K) → ℂ) (↑x : K) : ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) →
    w.embedding.toRatAlgHom = ψ
Tactic: rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 = ψ
⊢ Eq (α := IntermediateField ℚ K) ℚ⟮(↑x : K)⟯ ⊤
have rw₁ : ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits
Tactic: rw [Field.primitive_element_iff_algHom_eq_of_eval ℚ ℂ ?_ _ w.embedding.toRatAlgHom]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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) : ℂ)
⊢ w.embedding.toRatAlgHom = ψ
have h : LE.le (α := ℝ) (1 : ℝ) ((w : (a : K) → ℝ) (↑x : K) : ℝ)
Tactic: have h : 1 ≤ w x := one_le_of_lt_one h₁ h₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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) : ℝ)
⊢ w = mk ψ.toRingHom
have h₄ : 1 ≤ norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
Tactic: rw [← norm_embedding_eq, hψ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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) : ℂ)
⊢ w = mk ψ.toRingHom
have contrapose! : ∀ (h : w ≠ mk ψ.toRingHom), norm (E := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) < 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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.embedding.toRatAlgHom = ψ
have main : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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.toRatAlgHom = ψ
have main₁ : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
Tactic: rw [(mk_embedding w).symm, mk_eq_iff] at main
Cleared hypotheses: main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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.toRatAlgHom = ψ
have main₁ : w.embedding = ψ.toRingHom
Tactic: rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
Cleared hypotheses: main, hw
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
⊢ w.embedding.toRatAlgHom = ψ
have inr : ∀ (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom), 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
have rw : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
  ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
Tactic: rw [← Complex.conj_eq_iff_im]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
have this : Eq (α := ℂ) ((ComplexEmbedding.conjugate w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
  ((ψ.toRingHom : (a : K) → ℂ) (↑x : K) : ℂ)
Tactic: have := RingHom.congr_fun h' x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((ψ : (a : K) → ℂ) (↑x : K) : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ) : ℂ)
    ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
have rw : Eq (α := ℂ) ((ψ : (a : K) → ℂ) (↑x : K) : ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
Tactic: have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have inr : ∀ (h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ))
  (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
  (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
  1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h, main, hw, h', this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
inr :
  ∀ (h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ))
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have inr₁ : ∀
  (h :
    1 ≤
      ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) +
          (↑(Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) * Complex.I‖)
  (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
  (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
  1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h, main, hw, h', this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
inr :
  ∀ (h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ))
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₁ :
  ∀
    (h :
      1 ≤
        ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) +
            (↑(Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have inr₂ : ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + (↑0 : ℂ) * Complex.I‖)
  (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
  (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
  1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h, main, hw, h', this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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 : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0
inr :
  ∀ (h : 1 ≤ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) (↑x : K) : ℂ))
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₁ :
  ∀
    (h :
      1 ≤
        ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) +
            (↑(Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
inr₂ :
  ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + (↑0 : ℂ) * Complex.I‖)
    (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
    (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
    (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
    1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
⊢ 1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
have inr₃ : ∀ (h : 1 ≤ ‖(↑(Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))) : ℂ) + 0 * Complex.I‖)
  (main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1)
  (h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom)
  (this : Complex.im ((w.embedding : (a : K) → ℂ) (↑x : K)) = 0),
  1 ≤ |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))|
Tactic: rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h, main, hw, h', this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ
have inl : ∀ (hw : w.IsReal), w.embedding.toRatAlgHom = ψ
Tactic: cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h₃
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
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.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
inl : ∀ (hw : w.IsReal), w.embedding.toRatAlgHom = ψ
⊢ w.embedding.toRatAlgHom = ψ
have inr : ∀ (hw : |Complex.re ((w.embedding : (a : K) → ℂ) (↑x : K))| < 1), w.embedding.toRatAlgHom = ψ
Tactic: cases h₃ with
    | inl hw =>
      rw [conjugate_embedding_eq_of_isReal hw, or_self] at main
      exact congr_arg RingHom.toRatAlgHom main
    | inr hw =>
      refine congr_arg RingHom.toRatAlgHom (main.resolve_right fun h' ↦ hw.not_ge ?_)
      have : (embedding w x).im = 0 := by
        rw [← Complex.conj_eq_iff_im]
        have := RingHom.congr_fun h' x
        simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this
        rw [this]
        exact hψ.symm
      rwa [← norm_embedding_eq, ← Complex.re_add_im (embedding w x), this, Complex.ofReal_zero,
        zero_mul, add_zero, Complex.norm_real] at h
Cleared hypotheses: h₃