mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case e'_3
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ a' = ?convert_4 / gcd ?convert_4 ?convert_5

pp: case e'_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = ?convert_5 / gcd ?convert_4 ?convert_5

pp: case convert_3
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := ⋯
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ GCDMonoid k[X]

pp: case convert_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := ⋯
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ k[X]

pp: case convert_5
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := ⋯
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ k[X]

pp: case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ ?convert_5 ≠ 0

Tactic:
·

Goal state after:
case e'_3
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ a' = ?convert_4 / gcd ?convert_4 ?convert_5
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case e'_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = b / gcd a b

pp: case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b ≠ 0

Tactic:
·

Goal state after:
case e'_4
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b' = b / gcd a b
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b ≠ 0

Tactic:
·

Goal state after:
case convert_6
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ b ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ ∀ x ∈ Set.range ⇑(canonicalEmbedding K), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)

pp: case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)

pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ ∀ x ∈ Set.range ⇑(canonicalEmbedding K), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)

pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ (starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: case inl
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal ↥(⨆ i, k i)

pp: case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
·

Goal state after:
case inl
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal ↥(⨆ i, k i)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
·

Goal state after:
case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ IsTotallyReal ↥(⨆ i, k i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
·

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
·

Goal state after:
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

pp: case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r

pp: case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
·

Goal state after:
case inl.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
·

Goal state after:
case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (⇑Complex.measurableEquivRealProd.symm ⁻¹' {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2}) = 4 * ↑B ^ 2

pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ NullMeasurableSet {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} volume

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ volume (⇑Complex.measurableEquivRealProd.symm ⁻¹' {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2}) = 4 * ↑B ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : r < 0
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r →
    x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r}

pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r

Tactic:
·

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r →
    x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r

Tactic:
·

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ NullMeasurableSet {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} volume

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ NullMeasurableSet {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.re| 1

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.im| (↑B ^ 2)

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.re| 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.im| (↑B ^ 2)

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.im| (↑B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀,
          volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x))) *
        volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀))) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ ∏ x ∈ Finset.univ.erase w₀,
      volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x)) =
    ∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2

Tactic:
·

Goal state after:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ ∏ x ∈ Finset.univ.erase w₀,
      volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x)) =
    ∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2

Tactic:
·

Goal state after:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2

Tactic:
simpa only [ite_true] using vol_box (f w₀)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : w.IsReal
⊢ 2 ≤ 1

pp: case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : w.IsReal
⊢ 1 ≤ 1

pp: case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : (w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 1 ≤ 2

pp: case neg
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : ¬w.IsReal
⊢ 2 ≤ 2

Tactic:
·

Goal state after:
case pos
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h₁ : ¬(w.comap f).IsReal
h₂ : w.IsReal
⊢ 2 ≤ 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nontrivial (mixedSpace K)

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial (mixedSpace K)

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ Nontrivial (mixedSpace K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial (mixedSpace K)

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ Nontrivial (mixedSpace K)