mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
p : Primes
k : ℕ
⊢ χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1))) =
    χ ↑(↑p ^ (k + 1)) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log ↑(↑p ^ (k + 1))) * ↑(↑p ^ (k + 1)) ^ (-s)

Tactic:
simp

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
p : Primes
k : ℕ
⊢ χ ↑↑p ^ (k + 1) * (↑↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ((↑k + 1) * Complex.log ↑↑p) =
    χ ↑↑p ^ (k + 1) * ↑(Λ (↑p ^ (k + 1))) / ((↑k + 1) * Complex.log ↑↑p) * (↑↑p ^ (k + 1)) ^ (-s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2)
    (sinZeta (↑a) s)
⊢ (cexp (-(2 * ↑π * ↑a * ↑0) * I) - cexp (2 * ↑π * ↑a * ↑0 * I)) * I / 2 / ↑0 ^ s =
    -I * ↑(↑0).sign * cexp (2 * ↑π * I * ↑a * ↑0) / ↑0 ^ s / 2 +
      -(-I * ↑(↑0).sign) * cexp (-(2 * ↑π * I * ↑a * ↑0)) / ↑0 ^ s / 2

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaOdd a (-2 * ↑n - 1) = 0

Tactic:
by
  rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ 0 ≤ ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ (-s).re ≠ 0

Tactic:
simp

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ¬s.re = 0
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ↑n ^ (-s).re ≤ ↑n ^ (-s.re)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree ≤ ?b

pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ ?b < a.degree + b.degree

pp: case b
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ WithBot ℕ

Tactic:
· exact degree_mul_le a (derivative b)

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ ↑(Λ 0) / ↑(Real.log ↑0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ a * derivative b

Tactic:
hw

Goal state after:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative a * b
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ primeFactors 0 = ∅

Tactic:
by simp [primeFactors]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ primeFactors 1 = ∅

Tactic:
by simp [primeFactors]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ (↑(primeFactors 0)).Pairwise IsRelPrime

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ha : IsRadical 0
⊢ (normalizedFactors 0).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ C (↑i + 1) * (p ^ i * normalize p)

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ p ^ i * normalize p
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
⊢ radical (a ^ 0) ∣ radical a

Tactic:
simp

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

Goal state before:
pp: case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremFor n

Tactic:
apply FermatLastTheoremWith.mono hdvd

Goal state after:
case inl
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
hdvd : 4 ∣ n
⊢ FermatLastTheoremWith ℕ 4
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inr
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremFor n

Tactic:
apply FermatLastTheoremWith.mono hdvd

Goal state after:
case inr
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremWith ℕ p
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
⊢ radical a = 1 ↔ a = 0 ∨ IsUnit a

Tactic:
refine ⟨?_, (Or.elim · (by simp +contextual) radical_of_isUnit)⟩
  intro h
  rw [or_iff_not_imp_left]
  intro ha
  have : primeFactors a = ∅ := by rw [← primeFactors_radical, h, primeFactors_one]
  rwa [primeFactors_eq_empty_iff ha] at this

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
b : M
⊢ radical 0 ∣ radical b ↔ normalizedFactors 0 ⊆ normalizedFactors b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
b : M
hb₀ : b ≠ 0
h : 0 ∣ b
⊢ radical 0 ∣ radical b

Tactic:
simp

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

Goal state before:
pp: case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
hw

Goal state after:
case pos
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : 0 = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : 0 = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : w = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ (∃ n, a ∣ 0 ^ n) → radical a ∣ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
x✝ : radical a ∣ 0
⊢ a ∣ 0 ^ 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
h : (↑∅).Pairwise (Function.onFun IsRelPrime f)
⊢ radical (∏ i ∈ ∅, f i) = ∏ i ∈ ∅, radical (f i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
b : M
⊢ radical (0 * b) ∣ radical 0 * radical b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ radical (a * 0) ∣ radical a * radical 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
⊢ radical (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, radical (f i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : NormalizationMonoid R
inst✝ : UniqueFactorizationMonoid R
⊢ radical (-1) = 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ (↑ℤ (↑↑I).subtype).range ↔ x ∈ ↑↑I

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
ch0 : ringChar k = 0
⊢ a.natDegree = 0

pp: case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
⊢ a.natDegree = 0

Tactic:
· obtain ⟨da, -, -⟩ := flt_catalan_deriv
      hp hq hr hineq chp chq chr ha hb hc hab hu hv hw heq
    have czk : CharZero k := by
      apply charZero_of_inj_zero
      intro n
      rw [ringChar.spec, ch0]
      exact zero_dvd_iff.mp
    rw [eq_C_of_derivative_eq_zero da]
    exact natDegree_C _

Goal state after:
case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
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
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
chn0 : ringChar k ≠ 0
⊢ a.natDegree = 0
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
hw : ¬w.IsReal
⊢ w.embedding ≠ ComplexEmbedding.conjugate w.embedding

Tactic:
rwa [Ne, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]

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

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

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ |(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑x)| = 1

Tactic:
rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]

Goal state after:
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
x✝ : ch ≠ 1
hch2 : 2 ≤ ch
⊢ ca.natDegree + 1 ≤ ca.natDegree * ch

Tactic:
← hch2

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
x✝ : ch ≠ 1
hch2 : 2 ≤ ch
⊢ ca.natDegree + 1 ≤ ca.natDegree * 2
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
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (ComplexEmbedding.conjugate w.embedding) ↑x = ψ.toRingHom ↑x
⊢ (starRingEnd ℂ) (w.embedding ↑x) = w.embedding ↑x

Tactic:
simp only [ComplexEmbedding.conjugate_coe_eq, AlgHom.toRingHom_eq_coe,
          RingHom.coe_coe] at this

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
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (starRingEnd ℂ) (w.embedding ↑x) = ψ ↑x
⊢ (starRingEnd ℂ) (w.embedding ↑x) = w.embedding ↑x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w.IsReal ∨ w.IsComplex
⊢ w ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K

Tactic:
convert!
    Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K))
      (disjoint_isReal_isComplex K) using 1
  exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm

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

Goal state before:
pp: x : ℚ
w✝ : ℚ →+* ℂ
⊢ ↑⟨place w✝, ⋯⟩ x = ↑|x|

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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
x : K
hx : x ∈ E
φ : K →+* ℂ
⊢ φ x = (φ.comp E.subtype) ⟨x, hx⟩

Tactic:
simp

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
a✝¹ : InfinitePlace K
a✝ : a✝¹.IsComplex
h✝ : ⟨a✝¹, a✝⟩ = w₀
⊢ -x.2 ⟨a✝¹, a✝⟩ ∈ {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2} ↔ x.2 ⟨a✝¹, a✝⟩ ∈ {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2}

Tactic:
simp

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
a✝¹ : InfinitePlace K
a✝ : a✝¹.IsComplex
h✝ : ¬⟨a✝¹, a✝⟩ = w₀
⊢ -x.2 ⟨a✝¹, a✝⟩ ∈ ball 0 ↑(f a✝¹) ↔ x.2 ⟨a✝¹, a✝⟩ ∈ ball 0 ↑(f a✝¹)

Tactic:
simp

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:
simp

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:
simp

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
⊢ 0 ≤ 2

Tactic:
simp

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✝ : 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:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ (if hw : w.IsReal then ‖0.1 ⟨w, hw⟩‖ else ‖0.2 ⟨w, ⋯⟩‖) = 0

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ (if hw : w.IsReal then ‖1.1 ⟨w, hw⟩‖ else ‖1.2 ⟨w, ⋯⟩‖) = 1

Tactic:
simp

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : w.IsReal
⊢ ‖(x * y).1 ⟨w, h✝⟩‖ = ‖x.1 ⟨w, h✝⟩‖ * ‖y.1 ⟨w, h✝⟩‖

Tactic:
simp

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(x * y).2 ⟨w, ⋯⟩‖ = ‖x.2 ⟨w, ⋯⟩‖ * ‖y.2 ⟨w, ⋯⟩‖

Tactic:
simp

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : w.IsReal
⊢ ‖(-x).1 ⟨w, h✝⟩‖ = ‖x.1 ⟨w, h✝⟩‖

Tactic:
simp

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(-x).2 ⟨w, ⋯⟩‖ = ‖x.2 ⟨w, ⋯⟩‖

Tactic:
simp

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
h✝ : w.IsReal
⊢ ‖(c • x).1 ⟨w, h✝⟩‖ = |c| * ‖x.1 ⟨w, h✝⟩‖

Tactic:
simp

Goal state after: