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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
φ : { φ // ComplexEmbedding.IsReal φ }
⊢ (mk ↑φ).IsReal

pp: case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : (fun φ ↦ ⟨mk ↑φ, ⋯⟩) φ = (fun φ ↦ ⟨mk ↑φ, ⋯⟩) ψ
⊢ φ = ψ

pp: case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
φ : { φ // ComplexEmbedding.IsReal φ }
⊢ (mk ↑φ).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : (fun φ ↦ ⟨mk ↑φ, ⋯⟩) φ = (fun φ ↦ ⟨mk ↑φ, ⋯⟩) ψ
⊢ φ = ψ

pp: case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : (fun φ ↦ ⟨mk ↑φ, ⋯⟩) φ = (fun φ ↦ ⟨mk ↑φ, ⋯⟩) ψ
⊢ φ = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w

Tactic:
·

Goal state after:
case refine_3
K : Type u_1
inst✝ : Field K
w : { w // w.IsReal }
⊢ ∃ a, (fun φ ↦ ⟨mk ↑φ, ⋯⟩) a = w
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ‖∏ σ, σ x‖

pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖

Tactic:
·

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ‖∏ σ, σ x‖
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖

Tactic:
·

Goal state after:
case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mp
x y z : ℤ
⊢ PythagoreanTriple x y z →
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

pp: case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z

Tactic:
·

Goal state after:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z →
    ∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ (k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2) ∧ k * (2 * m * n) = k * (2 * m * n) ∨
      k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∧ k * (2 * m * n) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

pp: case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
·

Goal state after:
case h.inl
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ (k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2) ∧ k * (2 * m * n) = k * (2 * m * n) ∨
      k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∧ k * (2 * m * n) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ Finset.univ
⊢ 0 < x✝¹ ↑a ^ x✝¹.mult

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a ^ z.mult < 1

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ Finset.univ
⊢ 0 < x✝¹ ↑a ^ x✝¹.mult
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a ^ z.mult < 1

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ z ↑a ^ z.mult < 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
·

Goal state after:
case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
⊢ (k * (2 * m * n) = k * (m ^ 2 - n ^ 2) ∧ k * (m ^ 2 - n ^ 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧ k * (m ^ 2 - n ^ 2) = k * (m ^ 2 - n ^ 2)) ∧
    (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : z = w
⊢ z ↑a < 1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : ¬z = w
⊢ z ↑a < 1

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : z = w
⊢ z ↑a < 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : ¬z = w
⊢ z ↑a < 1

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
hz : ¬z = w
⊢ z ↑a < 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)).Finite

Tactic:
refine (Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
⊢ IsIntegral ℤ a

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ ca.natDegree ≤ d

pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
·

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ ca.natDegree ≤ d
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
⊢ IsIntegral ℤ a

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
⊢ IsIntegral ℤ a
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ 1 ≤ ↑|(Algebra.norm ℚ) ↑a|

Tactic:
rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast, Int.cast_le]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ 1 ≤ |(Algebra.norm ℤ) a|
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z

Tactic:
·

Goal state after:
case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
x✝ : a ∈ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) '' ↑(torsion K)
u : (𝓞 K)ˣ
h_tors : u ∈ ↑(torsion K)
h_ua : (fun x ↦ (algebraMap (𝓞 K) K) ↑x) u = a
φ : K →+* ℂ
⊢ ‖φ a‖ ≤ 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (ψ : K →ₐ[ℚ] ℂ), w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (ψ : K →ₐ[ℚ] ℂ), w.embedding.toRatAlgHom ↑x = ψ ↑x → w.embedding.toRatAlgHom = ψ
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k

pp: case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ torsionOrder K

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ torsionOrder K

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ torsionOrder K
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ torsionOrder K

Tactic:
have hζ : ζ ∈ torsion K := by
      rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
      exact ⟨k, k.prop, h⟩
    rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
    apply orderOf_dvd_natCard

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hle
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ

pp: case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))

Tactic:
·

Goal state after:
case hle
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))

Tactic:
·

Goal state after:
case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf ↑x
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf ↑x ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf ↑x
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf ↑x ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf ↑x ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case neg.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 0
hc : 0 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 1
hc : 1 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
·

Goal state after:
case neg.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 0
hc : 0 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case neg.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 1
hc : 1 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

pp: case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
·

Goal state after:
case neg.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 1
hc : 1 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
·

Goal state after:
case neg.«2»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 2
hc : 2 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
·

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
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
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #{φ | mkComplex φ = ⟨w, hw⟩} = #{φ | mk φ = w}

pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ 2 = w.mult

Tactic:
·

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #{φ | mkComplex φ = ⟨w, hw⟩} = #{φ | mk φ = w}
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x // mkComplex x = ⟨w, hw⟩ } → { x // mk x = w }

pp: case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ?e'_2.refine_1 x✝¹ = ?e'_2.refine_1 x✝
⊢ x✝¹ = x✝

pp: case e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a, ?e'_2.refine_1 a = ⟨φ, hφ⟩

Tactic:
·

Goal state after:
case e'_2.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ { x // mkComplex x = ⟨w, hw⟩ } → { x // mk x = w }