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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
h : contract (ringChar k) a = 0
⊢ False

Tactic:
rw [h, map_zero] at heq

Goal state after:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = 0
h : contract (ringChar k) a = 0
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
;

Goal state after:
case mpr.inr.inl.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2)

pp: case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
;

Goal state after:
case mpr.inr.inr.left
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2)

case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
;

Goal state after:
case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
;

Goal state after:
case mpr.inr.inr.right
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ = r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x = r

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ = r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x = r
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x ≤ r

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
φ : K →+* ℂ
⊢ ⟨place φ, ⋯⟩ x ≤ r
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
⊢ φ = ψ

Tactic:
;

Goal state after:
case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
⊢ φ = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
⊢ ComplexEmbedding.conjugate φ = ψ

Tactic:
;

Goal state after:
case mp.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
⊢ ComplexEmbedding.conjugate φ = ψ
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr.hi
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 : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
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
⊢ False

Tactic:
;

Goal state after:
case inr.hi
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 : ℕ
ih_d :
  ∀ m ≤ d,
    ∀ {a b c : k[X]},
      C u * a ^ p + C v * b ^ q + C w * c ^ r = 0 → a ≠ 0 → b ≠ 0 → c ≠ 0 → IsCoprime a b → a.natDegree = m → m = 0
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
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| {φ | mk φ = w}

Tactic:
;

Goal state after:
case s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| {φ | mk φ = w}
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| fun φ ↦ mk φ = w

pp: case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24

Tactic:
;

Goal state after:
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| fun φ ↦ mk φ = w

case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: x : 𝓞 ℚ
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1

Tactic:
;

Goal state after:
x : 𝓞 ℚ
⊢ ↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
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
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ (if z.IsReal then 1 else 2) ≠ 0

Tactic:
;

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
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ (if z.IsReal then 1 else 2) ≠ 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ orderOf ↑⟨-1, ⋯⟩ = 2

Tactic:
← orderOf_units,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ orderOf ↑↑⟨-1, ⋯⟩ = 2
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

Tactic:
← orderOf_units,

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.«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:
← orderOf_units,

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.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 }

Tactic:
exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
⊢ nrRealPlaces K = 0

Tactic:
refine (@Fintype.card_eq_zero_iff _ (_)).2 ⟨fun ⟨w, hwreal⟩ ↦ ?_⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : w.IsReal
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: a b : InfinitePlace ℚ
k✝ : ℚ
⊢ a k✝ = b k✝

Tactic:
;

Goal state after:
a b : InfinitePlace ℚ
k✝ : ℚ
⊢ a k✝ = b k✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: x✝ : ℚ
⊢ (star (castHom ℂ)) x✝ = (castHom ℂ) x✝

Tactic:
;

Goal state after:
x✝ : ℚ
⊢ (star (castHom ℂ)) x✝ = (castHom ℂ) x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ ¬n = 1
Module: Mathlib.NumberTheory.NumberField.EquivReindex

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

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ j✝ : K →+* ℂ
⊢ basisMatrix K i✝ j✝ =
    Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ) i✝ j✝
Module: Mathlib.NumberTheory.NumberField.EquivReindex

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

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i✝ j✝ : K →+* ℂ
⊢ (basisMatrix K).map (⇑(starRingEnd ℂ)) i✝ j✝ =
    (reindex (Equiv.refl (K →+* ℂ)) (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) (basisMatrix K) i✝ j✝
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:
basisMatrix_eq_embeddingsMatrixReindex,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ (Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)).det ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
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, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w ^ w.mult = B

Tactic:
← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁),

Goal state after:
case refine_2
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
⊢ Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) w₁ ^ w₁.mult *
      ∏ x ∈ Finset.univ.erase w₁, Function.update f w₁ ((B * S⁻¹) ^ (↑w₁.mult)⁻¹) x ^ x.mult =
    B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
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
⊢ ↑(if w₁.IsReal then 1 else 2) ≠ 0

Tactic:
;

Goal state after:
case refine_2
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
⊢ ↑(if w₁.IsReal then 1 else 2) ≠ 0
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
eq_lhs : n * n + n * n + n * n = 3 * n * n
⊢ 3 * (n * n) ≤ n * (n * n)

Tactic:
exact Nat.mul_le_mul_right (n * n) hn

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
x✝ : ℝ × ℝ
⊢ x✝ ∈ {a | |a.1| < 1 ∧ |a.2| < ↑B ^ 2} ↔ x✝ ∈ Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
B : ℝ≥0
x✝ : ℝ × ℝ
⊢ x✝ ∈ {a | |a.1| < 1 ∧ |a.2| < ↑B ^ 2} ↔ x✝ ∈ Set.Ioo (-1) 1 ×ˢ Set.Ioo (-↑B ^ 2) (↑B ^ 2)
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:
;

Goal state after:
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
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: 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}

Tactic:
;

Goal state after:
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: 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))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : K →+* ℂ
⊢ M i✝ j✝ = N.transpose i✝ j✝

Tactic:
;

Goal state after:
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))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
i✝ j✝ : K →+* ℂ
⊢ M i✝ j✝ = N.transpose i✝ j✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ⇑(latticeBasis K) = Set.range (⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(integralBasis K))

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ Set.range ⇑(latticeBasis K) = Set.range (⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap ∘ ⇑(integralBasis K))
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 ℤ (⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔
    x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range

Tactic:
← Submodule.map_span,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.map (canonicalEmbedding K).toIntAlgHom.toLinearMap (Submodule.span ℤ (Set.range ⇑(integralBasis K))) ↔
    x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
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
x : k
⊢ (place (w.embedding.comp f)) x = ((↑w).comp ⋯) x

Tactic:
;

Goal state after:
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
x : k
⊢ (place (w.embedding.comp f)) x = ((↑w).comp ⋯) x
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
x : k
⊢ (place (w.embedding.comp f)) x = ↑w (f x)

Tactic:
;

Goal state after:
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
x : k
⊢ (place (w.embedding.comp f)) x = ↑w (f x)
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
x : k
⊢ (place (w.embedding.comp f)) x = (place ⋯.choose) (f x)

Tactic:
;

Goal state after:
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
x : k
⊢ (place (w.embedding.comp f)) x = (place ⋯.choose) (f x)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inl
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
⊢ ∃ σ, σ • w = w'

Tactic:
obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h

Goal state after:
case inl
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
h : w.embedding.comp (algebraMap k K) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : w.embedding.comp ↑σ.symm = w'.embedding
⊢ ∃ σ, σ • w = w'
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✝ : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
⊢ w.embedding.comp (algebraMap k K) = (w.embedding.comp ↑σ.symm).comp (algebraMap k K)

Tactic:
;

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
⊢ w.embedding.comp (algebraMap k K) = (w.embedding.comp ↑σ.symm).comp (algebraMap k K)
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✝ : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
x✝ : k
⊢ (w.embedding.comp (algebraMap k K)) x✝ = ((w.embedding.comp ↑σ.symm).comp (algebraMap k K)) x✝

Tactic:
;

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : Gal(K/k)
x✝ : k
⊢ (w.embedding.comp (algebraMap k K)) x✝ = ((w.embedding.comp ↑σ.symm).comp (algebraMap k K)) x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k (star (star φ))

Tactic:
;

Goal state after:
case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k (star (star φ))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ ↑(Algebra.discr ℚ ⇑(integralBasis K)) = (basisMatrix K).det ^ 2

Tactic:
basisMatrix_eq_embeddingsMatrixReindex,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
⊢ ↑(Algebra.discr ℚ ⇑(integralBasis K)) =
    (Algebra.embeddingsMatrixReindex ℚ ℂ (⇑(integralBasis K) ∘ ⇑(equivReindex K)) (RingHom.equivRatAlgHom K ℂ)).det ^ 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k (star (star φ))

Tactic:
;

Goal state after:
case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k (star (star φ))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
a✝ : InfinitePlace K
⊢ a✝ ∈ univ ↔ a✝ ∈ image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ

Tactic:
;

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
a✝ : InfinitePlace K
⊢ a✝ ∈ univ ↔ a✝ ∈ image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ