awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : { w : InfinitePlace K // w.IsComplex }
rw :
  (if hw : (↑w : InfinitePlace K).IsReal then
      x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) (↑w : InfinitePlace K) hw)
    else (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x) =
    ‖x.2 w‖
rw₁ : (normAtPlace (↑w : InfinitePlace K) : (a : mixedSpace K) → ℝ) x = ‖x.2 w‖
rw₂ : ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) ⋯)‖ = ‖x.2 w‖
hw : (↑w : InfinitePlace K).IsComplex
rw₃ : ‖x.2 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) (↑w : InfinitePlace K) ⋯)‖ = ‖x.2 w‖
hw₁ : (↑w : InfinitePlace K).IsComplex
⊢ normAtComplexPlaces x (↑w : InfinitePlace K) = ‖x.2 w‖

Tactic:
rw [normAtComplexPlaces, dif_neg (not_isReal_iff_isComplex.mpr w.prop),
    normAtPlace_apply_of_isComplex]

Premises used: Iff.mpr, dif_neg, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, Subtype.prop, NumberField.InfinitePlace.not_isReal_iff_isComplex, NumberField.mixedEmbedding.normAtComplexPlaces
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
h : ∀ (w : InfinitePlace K), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) = x

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
h : ∀ (hw : w.IsReal), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
h₁ : ∀ (hw : w.IsComplex), normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsReal
h :
  ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
    x w
h₁ h₂ :
  (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
          fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).1
      (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw) =
    x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w

Tactic:
rw [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, mixedSpaceOfRealSpace_apply]

Premises used: Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
h :
  norm (E := ℂ)
      (((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
h₁ :
  norm (E := ℂ)
      ((fun (w : { w : InfinitePlace K // w.IsReal }) ↦ x (↑w : InfinitePlace K),
            fun (w : { w : InfinitePlace K // w.IsComplex }) ↦ (↑(x (↑w : InfinitePlace K)) : ℂ)).2
        (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsComplex) w hw)) =
    x w
h₂ h₃ : x w = x w
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w

Tactic:
rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply,
      Complex.norm_of_nonneg (hx w hw)]

Premises used: Complex.norm_of_nonneg, Subtype.mk, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
⊢ normAtAllPlaces x w = (normAtPlace w : (a : mixedSpace K) → ℝ) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Continuous.{u_1, u_1} (X := mixedSpace K) normAtAllPlaces

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
⊢ 0 ≤ normAtAllPlaces x w

Tactic:
normAtPlace_nonneg _ _

Premises used: NumberField.mixedEmbedding.normAtPlace_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
h :
  ∀ (x_1 : InfinitePlace K), normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) x_1 = x x_1
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 ≤ x w
x_1 : InfinitePlace K
h :
  (normAtPlace x_1 : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x x_1
h₁ h₂ : x x_1 = x x_1
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) x_1 = x x_1

Tactic:
rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hx _)]

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : K
w : InfinitePlace K
rw :
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) ((mixedEmbedding K : (a : K) → mixedSpace K) x : mixedSpace K) : ℝ)
    ((w : (a : K) → ℝ) x : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) ((w : (a : K) → ℝ) x : ℝ)
⊢ normAtAllPlaces ((mixedEmbedding K : (a : K) → mixedSpace K) x) w = (w : (a : K) → ℝ) x

Tactic:
rw [normAtAllPlaces_apply, normAtPlace_apply]

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, NumberField.mixedEmbedding.normAtPlace_apply
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x)) = normAtAllPlaces x

Tactic:
normAtAllPlaces_mixedSpaceOfRealSpace fun _ ↦ (normAtAllPlaces_nonneg _ _)

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_nonneg, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
h :
  ∀ (w : InfinitePlace K),
    normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) = normAtAllPlaces x

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
h :
  ∀ (hw : w.IsReal),
    normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
h₁ :
  ∀ (hw : w.IsComplex),
    normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
h :
  Eq (α := ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) : ℝ)
    ((normAtPlace w : (a : mixedSpace K) → ℝ) x : ℝ)
h₁ :
  ‖‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖‖ =
    ‖x.1 (Subtype.mk (p := fun (w : InfinitePlace K) ↦ w.IsReal) w hw)‖
⊢ normAtAllPlaces (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) w = normAtAllPlaces x w

Tactic:
simp_rw [normAtAllPlaces, normAtPlace_apply_of_isReal hw, norm_norm]

Premises used: NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, NumberField.mixedEmbedding.normAtAllPlaces, norm_norm
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x : mixedSpace K
⊢ normAtComplexPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) (normAtAllPlaces x)) =
    normAtAllPlaces x

Tactic:
normAtComplexPlaces_mixedSpaceOfRealSpace fun _ _ ↦ (normAtAllPlaces_nonneg _ _)

Premises used: NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.normAtAllPlaces_nonneg
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
h₁ : ∀ (w : InfinitePlace K), normAtAllPlaces x w = normAtAllPlaces y w
⊢ normAtAllPlaces x = normAtAllPlaces y

Tactic:
ext w
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
h₁ : ∀ (hw : w.IsReal), normAtAllPlaces x w = normAtAllPlaces y w
h₂ : ∀ (hw : w.IsComplex), normAtAllPlaces x w = normAtAllPlaces y w
⊢ normAtAllPlaces x w = normAtAllPlaces y w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Premises used: NumberField.InfinitePlace.isReal_or_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
hw : w.IsReal
⊢ normAtAllPlaces x w = normAtAllPlaces y w

Tactic:
simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isReal hw,
      normAtComplexPlaces_apply_isReal ⟨w, hw⟩] using congr_arg (|·|) (congr_fun h w)

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, abs, NumberField.mixedEmbedding.normAtPlace_apply_of_isReal, Subtype.mk, congr_arg, congr_fun, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
x y : mixedSpace K
h : normAtComplexPlaces x = normAtComplexPlaces y
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtAllPlaces x w = normAtAllPlaces y w

Tactic:
simpa [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
      normAtComplexPlaces_apply_isComplex ⟨w, hw⟩] using congr_fun h w

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, Subtype.mk, NumberField.mixedEmbedding.normAtPlace_apply_of_isComplex, congr_fun, NumberField.mixedEmbedding.normAtComplexPlaces_apply_isComplex
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
rw : s ⊆ Set.range normAtAllPlaces
⊢ normAtAllPlaces '' normAtAllPlaces ⁻¹' s = s

Tactic:
rw [Set.image_preimage_eq_iff]

Premises used: Set.image_preimage_eq_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
⊢ Membership.mem (γ := Set (realSpace K)) (Set.range normAtAllPlaces) x

Tactic:
⟨mixedSpaceOfRealSpace x, funext fun w ↦ ?_⟩

Premises used: Set.Mem, setOf, NumberField.mixedEmbedding.mixedSpaceOfRealSpace, funext, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
refine : ∀ (w : InfinitePlace K), normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w
⊢ Membership.mem (γ := Set (realSpace K)) (Set.range normAtAllPlaces) x

Tactic:
refine ⟨mixedSpaceOfRealSpace x, funext fun w ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
Goal:
K : Type u_1
inst : Field K
s : Set (realSpace K)
hs : ∀ x ∈ s, ∀ (w : InfinitePlace K), 0 ≤ x w
x : realSpace K
hx : x ∈ s
w : InfinitePlace K
rw :
  (normAtPlace w : (a : mixedSpace K) → ℝ)
      ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x : mixedSpace K) =
    x w
rw₁ rw₂ : x w = x w
⊢ normAtAllPlaces ((mixedSpaceOfRealSpace : (a : realSpace K) → mixedSpace K) x) w = x w

Tactic:
rw [normAtAllPlaces_apply, normAtPlace_mixedSpaceOfRealSpace (hs x hx w)]

Premises used: NumberField.mixedEmbedding.normAtAllPlaces_apply, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
simp :
  ∀
    (hx :
      (∀ (a : InfinitePlace K) (b : a.IsReal),
          |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
        ∀ (a : InfinitePlace K) (b : a.IsComplex),
          ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)),
    (∀ (a : InfinitePlace K) (b : a.IsReal),
        |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
      ∀ (a : InfinitePlace K) (b : a.IsComplex),
        ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)
⊢ -x ∈ convexBodyLT K f

Tactic:
simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
    mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
    Prod.snd_neg] at hx ⊢

Premises used: forall_true_left, Prod.snd_neg, Prod.fst_neg, Subtype.forall, Set.mem_pi, Set.mem_prod, norm_neg, Set.mem_univ, Pi.neg_apply, Real.norm_eq_abs, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)

Tactic:
hx
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal),
      |x.1 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsReal) a b)| < (↑(f a) : ℝ)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      ‖x.2 (Subtype.mk (p := fun (a : InfinitePlace K) ↦ a.IsComplex) a b)‖ < (↑(f a) : ℝ)

Tactic:
exact hx
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
⊢ Convex ℝ (convexBodyLT K f)

Tactic:
Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => convex_ball _ _))

Premises used: convex_pi, convex_ball, Convex.prod, OfNat.ofNat, Subtype.val, NNReal.toReal
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ convexBodyLTFactor K ≠ 0

Tactic:
mul_ne_zero (pow_ne_zero _ two_ne_zero) (pow_ne_zero _ pi_ne_zero)

Premises used: NNReal.pi_ne_zero, pow_ne_zero, two_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 1 ≤ convexBodyLTFactor K

Tactic:
one_le_mul (one_le_pow₀ one_le_two) (one_le_pow₀ (one_le_two.trans Real.two_le_pi))

Premises used: Real.two_le_pi, one_le_pow₀, one_le_two, one_le_mul, LE.le.trans
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ LE.le (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
⊢ ((↑2 : ℝ≥0∞) ^ nrRealPlaces K *
        ∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) *
      ((∏ x : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2) *
        (↑pi : ℝ≥0∞) ^ nrComplexPlaces K) =
    (↑2 : ℝ≥0∞) ^ nrRealPlaces K * (↑pi : ℝ≥0∞) ^ nrComplexPlaces K *
      HMul.hMul (α := ℝ≥0∞)
        (∏ x : { w : InfinitePlace K // w.IsReal }, ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ))
        (∏ x : { w : InfinitePlace K // w.IsComplex },
          HPow.hPow (β := ℕ) (ENNReal.ofReal (↑(f (↑x : InfinitePlace K)) : ℝ)) 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Tactic:
⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩

Premises used: Function.update, HMul.hMul, NumberField.InfinitePlace.mult, Nat.cast, Inv.inv, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
refine_1 :
  ∀ (w : InfinitePlace K),
    w ≠ w₁ →
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w =
        f w
refine_2 :
  ∏ w : InfinitePlace K,
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
        w.mult =
    B
⊢ ∃ (g : InfinitePlace K → ℝ≥0), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, g w ^ w.mult = B

Tactic:
refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∀ (w : InfinitePlace K),
    w ≠ w₁ →
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w =
        f w

Tactic:
fun w hw => Function.update_of_ne hw _ f

Premises used: HMul.hMul, NumberField.InfinitePlace.mult, Nat.cast, Inv.inv, HPow.hPow, Function.update_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∀ (w : InfinitePlace K),
    w ≠ w₁ →
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w =
        f w

Tactic:
exact fun w hw => Function.update_of_ne hw _ f

Premises used: Function.update_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.erase Finset.univ w₁
rw rw₁ : f w ^ w.mult = f w ^ w.mult
⊢ Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
      w.mult =
    f w ^ w.mult

Tactic:
rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)]

Premises used: Finset.ne_of_mem_erase, Function.update_of_ne
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
refine_2 : S ≠ 0
refine_2₁ : Ne (α := ℝ) (↑w₁.mult : ℝ) 0
⊢ ∏ w : InfinitePlace K,
      Function.update (β := fun (a : InfinitePlace K) ↦ ℝ≥0) f w₁ (HPow.hPow (β := ℝ) (B * S⁻¹) (↑w₁.mult : ℝ)⁻¹) w ^
        w.mult =
    B

Tactic:
rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_self,
      Finset.prod_congr rfl fun w hw => by rw [Function.update_of_ne (Finset.ne_of_mem_erase hw)],
      ← NNReal.rpow_natCast, ← NNReal.rpow_mul, inv_mul_cancel₀, NNReal.rpow_one, mul_assoc,
      inv_mul_cancel₀, mul_one]

Premises used: Finset.mem_univ, Finset.univ, NNReal.rpow_natCast, mul_assoc, NNReal.rpow_mul, Finset.mul_prod_erase, Finset.prod_congr, Function.update_self, mul_one, NNReal.rpow_one, inv_mul_cancel₀, rfl
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
refine_2 : ∀ a ∈ Finset.erase Finset.univ w₁, f a ^ a.mult ≠ 0
⊢ S ≠ 0

Tactic:
rw [Finset.prod_ne_zero_iff]

Premises used: Finset.prod_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.erase Finset.univ w₁, f a ^ a.mult ≠ 0

Tactic:
fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))

Premises used: NumberField.InfinitePlace.mult, pow_ne_zero, Finset.ne_of_mem_erase
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.erase Finset.univ w₁, f a ^ a.mult ≠ 0

Tactic:
exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))

Premises used: pow_ne_zero, Finset.ne_of_mem_erase
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
pos : w₁.IsReal → Ne (α := ℝ) (↑1 : ℝ) 0
neg : ¬w₁.IsReal → Ne (α := ℝ) (↑2 : ℝ) 0
⊢ Ne (α := ℝ) (↑(if w₁.IsReal then 1 else 2) : ℝ) 0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
Goal:
K : Type u_1
inst : Field K
f : InfinitePlace K → ℝ≥0
inst_1 : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.erase Finset.univ w₁, f w ^ w.mult
h : w₁.IsReal
⊢ Ne (α := ℝ) (↑1 : ℝ) 0

Tactic:
norm_num