awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) x
y : (𝓞 K)ˣ
hy_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y
hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) y
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1) :
      (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1) :
      (𝓞 K ⧸ I)ˣ)
rw :
  Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) x hx =
    Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) y hy
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1 =
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1

Tactic:
rw [Subtype.mk_eq_mk, ← Subtype.mk_eq_mk (h := hx) (h' := hy)]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) x
y : (𝓞 K)ˣ
hy_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y
hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) y
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1) :
      (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1) :
      (𝓞 K ⧸ I)ˣ)
⊢ Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) x hx =
    Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) y hy

Tactic:
rootsOfUnityMapQuot_injective (torsionOrder K) hI₁ hI₂ h

Premises used: Ideal.rootsOfUnityMapQuot_injective, Set.Mem, NumberField.Units.torsionOrder
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) x
y : (𝓞 K)ˣ
hy_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y
hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) y
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1) :
      (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1) :
      (𝓞 K ⧸ I)ˣ)
⊢ Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) x hx =
    Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) y hy

Tactic:
exact rootsOfUnityMapQuot_injective (torsionOrder K) hI₁ hI₂ h

Premises used: Ideal.rootsOfUnityMapQuot_injective, NumberField.Units.torsionOrder
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
⊢ P.IsMaximal

Tactic:
have : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hP₀ hP₁
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)

Tactic:
have hP₃ : absNorm P ≠ 1 := absNorm_eq_one_iff.not.mpr <| IsPrime.ne_top hP₁
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
⊢ Nat.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ

Tactic:
have h := Subgroup.card_dvd_of_injective _ (torsionMapQuot_injective hP₃ hP₂)
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
h : Nat.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ
rwa :
  ∀ (h : Fintype.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ),
    torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : Fintype.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P) - 1),
    torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)

Tactic:
rwa [Nat.card_eq_fintype_card, Nat.card_units] at h

Premises used: Nat.card_units, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.NumberField.Ideal.Basic
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
inst_2 : I.IsMaximal
⊢ Finite.{u_1 + 1} (𝓞 K ⧸ I)

Tactic:
I.finiteQuotientOfFreeOfNeBot (I.bot_lt_of_maximal (RingOfIntegers.not_isField K)).ne'

Premises used: NumberField.RingOfIntegers.not_isField, Ideal.bot_lt_of_maximal, LT.lt.ne', Ideal.finiteQuotientOfFreeOfNeBot
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Nontrivial.{u_1} (InfiniteAdeleRing K)

Tactic:
(inferInstance : Nonempty (InfinitePlace K)).elim fun w => Pi.nontrivial_at w

Premises used: Nonempty.elim, inferInstance, Pi.nontrivial_at
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
x : K
v : InfinitePlace K
⊢ Eq (α := v.Completion) ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x v : v.Completion)
    ((↑(WithAbs.toAbs (↑v : AbsoluteValue K ℝ) x) : UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ))) :
      UniformSpace.Completion (WithAbs (↑v : AbsoluteValue K ℝ)))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LocallyCompactSpace.{u_1} (InfiniteAdeleRing K)

Tactic:
Pi.locallyCompactSpace_of_finite

Premises used: NumberField.InfiniteAdeleRing, NumberField.instTopologicalSpaceInfiniteAdeleRing._aux_1, Pi.locallyCompactSpace_of_finite
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
x : InfiniteAdeleRing K
⊢ Eq (α := mixedEmbedding.mixedSpace K)
    ((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K) x : mixedEmbedding.mixedSpace K)
    ((fun (v : { w : InfinitePlace K // w.IsReal }) ↦
        (extensionEmbeddingOfIsReal ⋯ : (a : (↑v : InfinitePlace K).Completion) → ℝ) (x (↑v : InfinitePlace K)),
        fun (v : { w : InfinitePlace K // w.IsComplex }) ↦
        (extensionEmbedding (↑v : InfinitePlace K) : (a : (↑v : InfinitePlace K).Completion) → ℂ)
          (x (↑v : InfinitePlace K))) :
      ((v : { w : InfinitePlace K // w.IsReal }) → ℝ) × ((v : { w : InfinitePlace K // w.IsComplex }) → ℂ))

Tactic:
rfl

Premises used: NumberField.InfinitePlace.IsComplex, setOf, Prod.map, UniformSpace.Completion.extension, AbstractCompletion.extend, Not, rfl, ite
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
x : K
fst :
  ∀ (v : { w : InfinitePlace K // w.IsReal }),
    Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).1 v)
      (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
            ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).1
        v)
snd :
  ∀ (v : { w : InfinitePlace K // w.IsComplex }),
    Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).2 v)
      (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
            ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).2
        v)
⊢ Eq (α := mixedEmbedding.mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x : mixedEmbedding.mixedSpace K)
    ((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
        ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x) :
      mixedEmbedding.mixedSpace K)

Tactic:
ext v
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
x : K
v : { w : InfinitePlace K // w.IsReal }
⊢ Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).1 v)
    (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
          ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).1
      v)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
x : K
v : { w : InfinitePlace K // w.IsComplex }
⊢ Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).2 v)
    (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
          ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).2
      v)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DenseRange (X := InfiniteAdeleRing K) (α := K) (⇑(algebraMap K (InfiniteAdeleRing K)) : (a : K) → InfiniteAdeleRing K)

Tactic:
(DenseRange.piMap fun _ => UniformSpace.Completion.denseRange_coe).comp
    (InfinitePlace.denseRange_algebraMap_pi K)
      (.piMap fun _ => UniformSpace.Completion.continuous_coe _)

Premises used: UniformSpace.Completion.coe', WithAbs, NumberField.InfiniteAdeleRing, NumberField.instTopologicalSpaceInfiniteAdeleRing._aux_1, Continuous.piMap, UniformSpace.Completion.denseRange_coe, DenseRange.piMap, Pi.map, UniformSpace.Completion.continuous_coe, NumberField.InfinitePlace.denseRange_algebraMap_pi, SeparationQuotient.mk, DenseRange.comp, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
⊢ ‖x‖ = ∏ v : InfinitePlace K, ‖x v‖ ^ v.mult

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
hx : ¬IsUnit x
⊢ ∃ (x_1 : InfinitePlace K), ¬IsUnit (x x_1)

Tactic:
rw [Pi.isUnit_iff, not_forall] at hx

Premises used: Pi.isUnit_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
hx : ∃ (x_1 : InfinitePlace K), ¬IsUnit (x x_1)
obtain : ∀ (v : InfinitePlace K) (hv : ¬IsUnit (x v)), ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
obtain ⟨v, hv⟩ := hx
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
v : InfinitePlace K
hv : ¬IsUnit (x v)
⊢ ‖x v‖ ^ v.mult = 0

Tactic:
simpa [isUnit_iff_ne_zero] using hv

Premises used: isUnit_iff_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
v : InfinitePlace K
hv : ¬IsUnit (x v)
⊢ ‖x‖ = 0

Tactic:
exact Finset.prod_eq_zero_iff.2 ⟨v, Finset.mem_univ v, by simpa [isUnit_iff_ne_zero] using hv⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.prod_eq_zero_iff, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
⊢ norm (E := InfiniteAdeleRing K)
      ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x : InfiniteAdeleRing K) =
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) x| : ℝ)

Tactic:
simpa [-Rat.cast_abs, norm_def] using InfinitePlace.prod_eq_abs_norm x

Premises used: Rat.cast_abs, NumberField.InfiniteAdeleRing.norm_def, NumberField.InfinitePlace.prod_eq_abs_norm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Nonempty.{max 1 (u_1 + 1)} (K →+* ℂ)
⊢ Nonempty.{u_1 + 1} (InfinitePlace K)

Tactic:
Set.instNonemptyRange _

Premises used: Set.instNonemptyRange, Set.Mem, setOf, NumberField.InfinitePlace, Set.range
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
⊢ IsInfinitePlace (↑v : AbsoluteValue K ℝ)

Tactic:
simp [IsInfinitePlace, v.prop]

Premises used: NumberField.IsInfinitePlace, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : AbsoluteValue K ℝ
⊢ IsInfinitePlace v ↔ ∃ (w : InfinitePlace K), (↑w : AbsoluteValue K ℝ) = v

Tactic:
⟨fun H ↦ ⟨⟨v, H⟩, rfl⟩, fun ⟨w, hw⟩ ↦ hw ▸ w.isInfinitePlace⟩

Premises used: _private.0.NumberField.isInfinitePlace_iff.match_1, Eq.rec, NumberField.InfinitePlace.isInfinitePlace, Subtype.mk, NumberField.IsInfinitePlace, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v : InfinitePlace K
x : K
⊢ Eq (α := ℝ) ((v : (a : K) → ℝ) x : ℝ) (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : ∀ (k : K), Eq (α := ℝ) ((v₁ : (a : K) → ℝ) k : ℝ) ((v₂ : (a : K) → ℝ) k : ℝ)
⊢ v₁ = v₂

Tactic:
Subtype.ext <| AbsoluteValue.ext h

Premises used: AbsoluteValue.ext, NumberField.InfinitePlace, Subtype.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
⊢ (mk φ : (a : K) → ℝ) x = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ mk w.embedding = w

Tactic:
Subtype.ext w.2.choose_spec

Premises used: Exists.choose_spec, NumberField.InfinitePlace, Subtype.property, Subtype.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ

Tactic:
DFunLike.ext _ _ (fun x => ?_)

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
refine : ∀ (x : K), Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ

Tactic:
refine DFunLike.ext _ _ (fun x => ?_)

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
rw : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
rw₁ : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
rw₂ :
  norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
rw₃ rw₄ : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
⊢ Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)

Tactic:
rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]

Premises used: Complex.norm_conj, NumberField.ComplexEmbedding.conjugate_coe_eq, NumberField.InfinitePlace.apply
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
nth_rewrite : norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (mk w.embedding : (a : K) → ℝ) x
⊢ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x

Tactic:
nth_rewrite 2 [← mk_embedding w]

Premises used: NumberField.InfinitePlace.mk_embedding
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
⊢ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (mk w.embedding : (a : K) → ℝ) x

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x x_1 : InfinitePlace K
h : x.embedding = x_1.embedding
⊢ x = x_1

Tactic:
simpa using congr_arg mk h

Premises used: NumberField.InfinitePlace.mk, congr_arg
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
⊢ v₁.embedding = v₂.embedding ↔ v₁ = v₂

Tactic:
(embedding_injective _).eq_iff

Premises used: Function.Injective.eq_iff, NumberField.InfinitePlace.embedding_injective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Function.Injective (β := K →+* ℂ) fun (v : InfinitePlace K) ↦ ComplexEmbedding.conjugate v.embedding

Tactic:
star_injective.comp <| embedding_injective K

Premises used: star_injective, Function.Injective.comp, NumberField.InfinitePlace.embedding_injective
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
rw : mk v₁.embedding = v₂
rw₁ : mk (ComplexEmbedding.conjugate v₂.embedding) = v₂
rw₂ : mk v₂.embedding = v₂
rw₃ rw₄ : v₂ = v₂
⊢ v₁ = v₂

Tactic:
rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_conjugate_eq
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = r
φ : K →+* ℂ
⊢ (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) (place φ) ⋯ : (a : K) → ℝ) x = r

Tactic:
hφ φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = r
φ : K →+* ℂ
⊢ (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) (place φ) ⋯ : (a : K) → ℝ) x = r

Tactic:
exact hφ φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
φ : K →+* ℂ
⊢ (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) (place φ) ⋯ : (a : K) → ℝ) x ≤ r

Tactic:
hφ φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) ≤ r
φ : K →+* ℂ
⊢ (Subtype.mk (p := fun (w : AbsoluteValue K ℝ) ↦ ∃ (φ : K →+* ℂ), place φ = w) (place φ) ⋯ : (a : K) → ℝ) x ≤ r

Tactic:
exact hφ φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) x : ℝ) ↔ x ≠ 0

Tactic:
AbsoluteValue.pos_iff w.1

Premises used: AbsoluteValue.pos_iff, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
rw : φ = (mk φ).embedding ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
rw₁ : φ = (mk φ).embedding ∨ ComplexEmbedding.conjugate φ = (mk φ).embedding
rw₂ : mk φ = mk (mk φ).embedding
rw₃ rw₄ : mk φ = mk φ
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

Tactic:
rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.mk_eq_iff, eq_comm
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ

Tactic:
have := embedding_mk_eq φ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
rwa : ∀ (this : (mk φ).embedding = φ ∨ (mk φ).embedding = φ), (mk φ).embedding = φ
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (mk φ).embedding = φ), (mk φ).embedding = φ
⊢ (mk φ).embedding = φ

Tactic:
rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this

Premises used: Iff.mp, NumberField.ComplexEmbedding.isReal_iff, or_self
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

Tactic:
⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.embedding, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
refine : w.IsReal → ComplexEmbedding.IsReal w.embedding
⊢ w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ rwa rwa₁ rwa₂ rwa₃ : ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
rwa [embedding_mk_eq_of_isReal hφ]

Premises used: NumberField.InfinitePlace.embedding_mk_eq_of_isReal
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

Premises used: NumberField.InfinitePlace.mk_embedding, NumberField.InfinitePlace.embedding, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
refine : w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
contrapose : ∀ (hφ : ComplexEmbedding.IsReal (mk φ).embedding), ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
contrapose hφ
-- Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : (mk φ).embedding = φ
inl inl₁ inl₂ inl₃ : ∀ (hφ : ComplexEmbedding.IsReal φ) (h : (mk φ).embedding = φ), ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
rwa [h] at hφ