mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_4
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
⊢ Summable fun i ↦ ∫ (a_1 : ℝ) in Ioi 0, ‖↑a_1 ^ (s - 1) * (a i * ↑(rexp (-p i * a_1)))‖ ∂volume

Tactic:
· -- summability of integrals of norms
    apply Summable.of_norm
    convert! h_sum.mul_left (Real.Gamma s.re) using 2 with i
    simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc, norm_mul (a i), integral_const_mul]
    rw [← mul_div_assoc, mul_comm (Real.Gamma _), mul_div_assoc, norm_mul ‖a i‖, norm_norm]
    rcases hp i with hai | hpi
    · simp [hai]
    congr 1
    have := Real.integral_rpow_mul_exp_neg_mul_Ioi hs hpi
    simp_rw [← neg_mul (p i), one_div, inv_rpow hpi.le, ← div_eq_inv_mul] at this
    rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]
    refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
    rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
⊢ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-min p q * t)

Tactic:
have : F_int 1 a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
this : F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t
⊢ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-min p q * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
⊢ ContinuousOn (fun p ↦ jacobiTheta₂' p.1 p.2) V

Tactic:
let u (n : ℤ) : ℝ := 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|))

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ ContinuousOn (fun p ↦ jacobiTheta₂' p.1 p.2) V
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

Tactic:
· simp [hs]

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

Goal state before:
pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

Tactic:
rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
    · ring_nf
    all_goals rw [arg_ofReal_of_nonneg (abs_nonneg _)]; linarith [pi_pos]

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

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖↑(evenKernel a x) - ↑(if a = 0 then 1 else 0)‖

Tactic:
apply_ite ((↑) : ℝ → ℂ),

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
x : ℝ
| ‖↑(evenKernel a x) - if a = 0 then ↑1 else ↑0‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
⊢ completedCosZeta (↑a) s = mellin (fun t ↦ (↑(cosKernel (↑a) t) - 1) / 2) (s / 2)

Tactic:
mellin_div_const,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
⊢ completedCosZeta (↑a) s = mellin (fun t ↦ ↑(cosKernel (↑a) t) - 1) (s / 2) / 2
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 2 * ↑N₀ ≤ ↑m * ↑(2 * N₀).sqrt + 2 * ↑N₀ * S
⊢ 1 / 2 ≤ S

Tactic:
rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case a
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) p

Tactic:
refine (indicator_of_mem ?_ fun n : ℕ ↦ (1 / n : ℝ)).symm

Goal state after:
case a
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | Nat.Prime p} ∩ {p | k ≤ p}
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ ¬LSeriesSummable (fun n ↦ χ ↑n) 1

Tactic:
refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_
  refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity))
    (fun n ↦ ?_)
  simp only [norm_term_eq, Set.indicator, Set.mem_ofPred_eq]
  split_ifs with h₁ h₂
  · simp [h₂]
  · simp [h₁, χ.map_one]
  all_goals positivity

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ completedHurwitzZetaEven (↑a) s = mellin (fun t ↦ (↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2) (s / 2)

Tactic:
mellin_div_const,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ completedHurwitzZetaEven (↑a) s = mellin (fun t ↦ ↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) (s / 2) / 2
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Goal state after:
case inr.inl.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : c < 0
⊢ False

case inr.inl.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : b < 0
hc : 0 < c
⊢ False
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Goal state after:
case inr.inl.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : c < 0
⊢ False

case inr.inl.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : a < 0
hb : 0 < b
hc : 0 < c
⊢ False
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Goal state after:
case inr.inr.inl.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : c < 0
⊢ False

case inr.inr.inl.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : b < 0
hc : 0 < c
⊢ False
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
⊢ False

Tactic:
obtain hc | hc := hc.lt_or_gt

Goal state after:
case inr.inr.inr.inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : c < 0
⊢ False

case inr.inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))

Tactic:
have : ¬IsUnit (p : ZMod N) := by rwa [ZMod.isUnit_prime_iff_not_dvd h, not_not]

Goal state after:
case pos
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ = (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ ↑(x.gcd y) ∣ z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))

Tactic:
have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case hg
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ Summable fun x ↦ ↑x ^ (-s.re)

pp: case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ ↑i ^ (-s.re)

Tactic:
· simp [hs]

Goal state after:
case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ ↑i ^ (-s.re)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (L (fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n)) s) = L (fun n ↦ χ ↑n) s

Tactic:
← eulerProduct_log_eq_LSeries χ hs,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = L (fun n ↦ χ ↑n) s
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: case succ
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
n✝ : ℕ
⊢ divRadical (p ^ (n✝ + 1)) ∣ derivative (p ^ (n✝ + 1))

Tactic:
· case succ i =>
      rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical,
        radical_pow_of_prime hp i.succ_ne_zero, derivative_pow_succ, ← mul_assoc]
      apply dvd_mul_of_dvd_left
      rw [mul_comm, mul_assoc]
      apply dvd_mul_of_dvd_right
      rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
by
  have ab_nz := mul_ne_zero ha hb
  have abc_nz := mul_ne_zero ab_nz hc
  -- bound the degree of `divRadical (a * b * c)` using Wronskian `w`
  set abc_dr := divRadical (a * b * c)
  have abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree := by
    calc
      abc_dr.natDegree ≤ w.natDegree := Polynomial.natDegree_le_of_dvd abc_dr_dvd_w hw
      _ < a.natDegree + b.natDegree := by rw [wab] at hw ⊢; exact natDegree_wronskian_lt_add hw
  -- add the degree of `radical (a * b * c)` to both sides and rearrange
  set abc_r := radical (a * b * c)
  apply Nat.lt_of_add_lt_add_left
  calc
    a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
      rw [mul_comm _ (radical _), radical_mul_divRadical]
    _ = abc_dr.natDegree + abc_r.natDegree := by
      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
      exact Nat.add_lt_add_right abc_dr_ndeg_lt _

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
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have hCw := C_ne_zero.mpr hw

Goal state after:
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
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: case hb
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑I.den| ≠ 0

Tactic:
simp [Algebra.norm_eq_zero_iff]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: case hd
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑a| ≠ 0

Tactic:
simp [Algebra.norm_eq_zero_iff]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ ¬↑|(Algebra.norm ℤ) ↑I.den| = 0

Tactic:
simp [Algebra.norm_eq_zero_iff]

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_1
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
⊢ DenseRange ι

Tactic:
let j : { x // x ∈ closure (id '' K) } → (K.topologicalClosure : Set ℂ) :=
      fun x =>
      ⟨x, by
        convert! x.prop
        simp only [id, Set.image_id']
        rfl ⟩

Goal state after:
case refine_1
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
j : { x // x ∈ closure (id '' ↑K) } → ↑↑K.topologicalClosure := fun x ↦ ⟨↑x, ⋯⟩
⊢ DenseRange ι
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ

Tactic:
rw [← mk_conjugate_eq]
      exact congr_arg mk h

Goal state after:
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 →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w = mk ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
(mk_embedding w).symm,

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 →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : mk w.embedding = mk ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ
Module: Mathlib.NumberTheory.NumberField.EquivReindex

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

Tactic:
← Algebra.discr_reindex ℚ (integralBasis K) (equivReindex K).symm

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 ^ 2 =
    (algebraMap ℚ ℂ) (Algebra.discr ℚ (⇑(integralBasis K) ∘ ⇑(equivReindex K).symm.symm))
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
⊢ n * n + n * n + n * n ≤ n * n * n

Tactic:
eq_lhs,

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

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

Tactic:
iSup_of_empty

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

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

Tactic:
exact ⟨x, ⟨SetLike.coe_mem x, fun φ => (heq _).mp hx φ⟩, rfl⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

Tactic:
classical
  have : 0 ≤ (discr K : ℂ) ↔ Even (nrComplexPlaces K) := by
    rw [discr_eq_basisMatrix_det_sq, Complex.sq_nonneg_iff, ← conj_eq_iff_im, RingHom.map_det,
      RingHom.mapMatrix_apply, conj_basisMatrix, reindex_apply, Equiv.refl_symm, Equiv.coe_refl,
      Function.Involutive.toPerm_symm, det_permute', mul_eq_right₀,
      ComplexEmbedding.conjugate_sign]
    · simp only [Units.val_pow_eq_pow_val, Units.val_neg, Units.val_one, Int.reduceNeg,
        Int.cast_pow, Int.cast_neg, Int.cast_one]
      rw [neg_one_pow_eq_one_iff_even (by norm_num)]
    · exact det_of_basisMatrix_non_zero K
  obtain h | h | h := Int.lt_trichotomy 0 (discr K)
  · rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg h.le)]
  · grind [discr_ne_zero]
  · rw [Int.sign_eq_neg_one_of_neg h, Odd.neg_one_pow]
    rwa [← Nat.not_even_iff_odd, ← this, Int.cast_nonneg_iff, not_le]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ ‖x‖ ≤ B

Tactic:
exact le_trans (norm_le_convexBodySumFun x) hx

Goal state after: