mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
⊢ v ↑n = ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
z : ℤ
⊢ v ↑z = ‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
⊢ IsCoprime c a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
n : ℕ
hn : 1 < n
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
n : ℕ
hn : 1 < n
⊢ ↑n ≠ 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
n : ℕ
hn : 1 < n
⊢ ↑n ^ t = ↑n ^ 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
⊢ t = 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
h✝ : (↑w).IsEquiv ↑v
t : ℝ
left✝ : 0 < t
h : (fun x ↦ ↑w x ^ t) = ⇑↑v
k : K
⊢ w k = v k

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
⊢ w = v ↔ (↑w).IsEquiv ↑v

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ 1 < v ↑n

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ ↑v ↑n ≠ 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
⊢ (↑v).IsNontrivial

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (K →+* ℂ) = Fintype.card (ChooseBasisIndex ℤ (𝓞 K))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ basisMatrix K =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (basisMatrix K).map ⇑(starRingEnd ℂ) =
    (reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) (basisMatrix K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (mixedEmbedding K) x ∈ convexBodyLT K f ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ (basisMatrix K).det ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
⊢ -x ∈ convexBodyLT K f

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
⊢ (canonicalEmbedding K) α = (basisMatrix K)ᵀ *ᵥ fun i ↦ ↑((((integralBasis K).reindex (equivReindex K).symm).repr α) i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.EquivReindex

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ((basisMatrix K)ᵀ⁻¹ *ᵥ fun j ↦ (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i =
    ↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ 0 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi =
    (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ (↑2 ^ nrRealPlaces K * ∏ x, ENNReal.ofReal ↑(f ↑x)) * ((∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) * ↑pi ^ nrComplexPlaces K) =
    ↑(convexBodyLTFactor K) * ((∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ ↑(convexBodyLTFactor K) * ((∏ x, ENNReal.ofReal ↑(f ↑x)) * ∏ x, ENNReal.ofReal ↑(f ↑x) ^ 2) =
    ↑(convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
⊢ volume (convexBodyLT K f) = ↑(convexBodyLTFactor K) * ↑(∏ w, f w ^ w.mult)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
w : InfinitePlace K
hw : w ∈ Finset.univ.erase w₁
⊢ Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = ?m.102 w

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
⊢ ∃ g, (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w, g w ^ w.mult = B

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
⊢ 0 < n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
⊢ 1 = C 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
hone : 1 = C 1
⊢ -1 = C (-1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hn' : 0 < n
hone : 1 = C 1
hneg_one : -1 = C (-1)
heq : C 1 * a ^ n + C 1 * b ^ n + C (-1) * c ^ n = 0
⊢ n * n + n * n + n * n = 3 * n * n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : a ^ n + b ^ n = c ^ n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

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

Tactic:
by

Goal state after:
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 }
x : K
x✝ :
  (∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
h₁ : ∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)
w : InfinitePlace K
h_ne : w ≠ ↑w₀
hw : ¬w.IsReal
h₂ : if ⟨w, ⋯⟩ = w₀ then |(w.embedding x).re| < 1 ∧ |(w.embedding x).im| < ↑(f w) ^ 2 else w x < ↑(f w)
⊢ ¬⟨w, ⋯⟩ = w₀

Tactic:
by

Goal state after:
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 }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = ↑w₀
⊢ ¬⟨w, hw⟩ = w₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: 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
goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
⊢ FermatLastTheoremWith' k[X] n

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrComplexPlaces K = 0 ↔ IsTotallyReal K

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : IsTotallyReal K
inst✝¹ : Algebra F K
inst✝ : Algebra.IsAlgebraic F K
w : InfinitePlace F
⊢ w.IsReal

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyReal K
⊢ finrank ℚ K = nrRealPlaces K

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
v : InfinitePlace ℚ
⊢ v.IsReal

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
K : Type u_2
inst✝¹ : Field K
inst✝ : CharZero K
⊢ IsTotallyReal ↥⊥

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ (a✝ * b✝)) = x✝ (a✝ * b✝)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
⊢ 1 ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ (a✝ + b✝)) = x✝ (a✝ + b✝)

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
⊢ 0 ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
⊢ ∀ {x : K}, x ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x} → -x ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
⊢ ∀ x ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}, x⁻¹ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}

Tactic:
by

Goal state after:
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 }
x : K
⊢ (mixedEmbedding K) x ∈ convexBodyLT' K f w₀ ↔
    (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
      |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
E : Subfield K
inst✝ : IsTotallyReal ↥E
⊢ E ≤ maximalRealSubfield K

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
w : InfinitePlace ↥(maximalRealSubfield K)
⊢ w.IsReal

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
⊢ IsTotallyReal ↥E ↔ E ≤ maximalRealSubfield K

Tactic:
by

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

Goal state before:
pp: F✝ : Type u_1
inst✝³ : Field F✝
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal ↥E
hF : IsTotallyReal ↥F
⊢ IsTotallyReal ↥(E ⊔ F)

Tactic:
by

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

Goal state before:
pp: 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)
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
h : maximalRealSubfield K = ⊤
⊢ IsTotallyReal K

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrRealPlaces K = 0 ↔ IsTotallyComplex K

Tactic:
by

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

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyComplex K
⊢ finrank ℚ K = 2 * nrComplexPlaces K

Tactic:
by

Goal state after:
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 }
x : mixedSpace K
hx : x ∈ convexBodyLT' K f w₀
⊢ -x ∈ convexBodyLT' K f w₀

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ ↦ ‖φ x‖₊

Tactic:
by

Goal state after:
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 }
⊢ Convex ℝ (convexBodyLT' K f w₀)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
⊢ ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
by

Goal state after:
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 {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
this : M.det ≠ 0
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (latticeBasis K) i = (canonicalEmbedding K) ((integralBasis K) i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(latticeBasis K))

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
F : Type u_3
inst✝ : Field F
w : InfinitePlace K
f : k →+* K
⊢ place (w.embedding.comp f) = (↑w).comp ⋯

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
v : InfinitePlace k
w : InfinitePlace K
f : k →+* K
h : w.comap f = v
x : k
⊢ w (f x) = v x

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
⊢ (mk (lift K φ)).comap (algebraMap k K) = mk φ

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ (w.comap f).IsReal

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hf : (w.comap f).IsComplex
⊢ w.IsComplex

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap
    ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k ≃+* K
w : InfinitePlace K
⊢ (w.comap ↑f).IsReal ↔ w.IsReal

Tactic:
by

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

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
w : InfinitePlace k
⊢ (fun x ↦ x.comap (algebraMap k K)) (mk (lift K w.embedding)) = w

Tactic:
by

Goal state after:
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
⊢ volume (convexBodyLT' K f w₀) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
by

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

Goal state before:
pp: 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
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
by

Goal state after: