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

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
⊢ 0 < f ↑y

Tactic:
have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)
  have hxy' : abscissaOfAbsConv a < max x y + 1 := hx.trans_lt <| mod_cast hxy
  have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
    simp only [Set.mem_ofPred_eq, add_re, ofReal_re, one_re, hxy]
  have hfx : 0 < f (max x y + 1) := by
    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
  refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)
  · have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
    simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using
      iteratedDeriv_alternating ha₀ hxy' n
  · exact_mod_cast (le_max_right x y).trans (lt_add_one _).le

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_2
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num

Tactic:
rw [← q.den_eq_one_iff.mp (Nat.cast_eq_one.mp hd)] at h
    simpa only [Rat.den_intCast, Nat.cast_one, one_pow, mul_one] using! (abs_lt.mp h).1

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

Goal state before:
pp: case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
this : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
⊢ (fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ rexp (-(π * a ^ 2) * t)

Tactic:
simpa only [neg_mul π (a ^ 2), mul_one] using! (isBigO_refl _ _).mul isBigO_one_aux

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

Goal state before:
pp: case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) → 0 < τ.im

Tactic:
← summable_jacobiTheta₂_term_iff (z := z)

Goal state after:
case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) → Summable fun x ↦ jacobiTheta₂_term x z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → 0 < τ.im

Tactic:
← summable_jacobiTheta₂_term_iff (z := z)

Goal state after:
case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) → Summable fun x ↦ jacobiTheta₂_term x z τ
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}
⊢ IsOpen V

Tactic:
refine ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _ isOpen_Iio).prod ?_

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}
⊢ IsOpen {v | T < v.im}
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2)) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]

Goal state after:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂_term, Complex.exp_add]
  suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
  rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]

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

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]

Goal state after:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ ∑' (n : ℤ), jacobiTheta₂'_term n (z + τ) τ =
    cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
funext this,

Goal state after:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ ∑' (x : ℤ),
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (x + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (x + 1) z τ) =
    cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I *
      (cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (jacobiTheta₂' (z * -1 / τ) (-1 / τ) + z * jacobiTheta₂ (z * -1 / τ) (-1 / τ) * (2 * ↑π * I)))

Tactic:
mul_neg_one,

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I *
      (cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (jacobiTheta₂' (-z / τ) (-1 / τ) + z * jacobiTheta₂ (-z / τ) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-↑π * I * z ^ 2 / τ) *
        -(jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * -1 / τ) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))

Tactic:
mul_neg_one,

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-↑π * I * z ^ 2 / τ) *
        -(jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (-(↑π * I * z ^ 2) / τ) *
        (-jacobiTheta₂' (z / τ) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 0
⊢ riemannZeta s = (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * Gamma (s / 2 + 1))

Tactic:
· rw [riemannZeta_eq_completedRiemannZeta₀ hs, Gamma_add_one (s / 2) (by grind)]
    field

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

Goal state before:
pp: s : ℂ
⊢ riemannZeta s = (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * Gamma (s / 2 + 1))

Tactic:
rcases eq_or_ne s 0 with rfl | hs
  · simp [riemannZeta_zero]
  · rw [riemannZeta_eq_completedRiemannZeta₀ hs, Gamma_add_one (s / 2) (by grind)]
    field

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
rw [Summable.tsum_eq_zero_add] at this

Goal state after:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = 1 / ↑0 ^ s + ∑' (b : ℕ), 1 / ↑(b + 1) ^ s
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ Summable fun n ↦ 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.Dirichlet

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

Tactic:
← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
          LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L ((fun n ↦ χ ↑n) ⍟ ((fun n ↦ χ ↑n) * fun n ↦ ↑(μ n))) s = 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
mul_neg_one,

Goal state after:
case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I =
    -I * cexp (2 * ↑π * I * ↑a * ↑n) + - -I * cexp (2 * ↑π * I * ↑a * -↑n)
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
⊢ ∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = L (fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n)) s

Tactic:
tsum_congr (fun p ↦ (hasSum_taylorSeries_neg_log' (hpow_le p)).tsum_eq.symm),

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
⊢ ∑' (b : Primes) (b_1 : ℕ), (χ ↑↑b * ↑↑b ^ (-s)) ^ (b_1 + 1) / (↑b_1 + 1) =
    L (fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n)) s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ False

Tactic:
have h2m : (p : ℤ) ∣ 2 * m ^ 2 := by
    convert! dvd_add hp2 hp1 using 1
    ring

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ False
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: 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 : w = a.wronskian b
⊢ IsCoprime b c

Tactic:
rw [add_eq_zero_iff_neg_eq] at hsum

Goal state after:
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
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b c
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : primeFactors a = primeFactors b
⊢ radical a = radical b

Tactic:
by simp [radical, h]

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Tactic:
← IsCoprime.pow_iff hp.bot_lt hq.bot_lt,

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (a ^ p) (b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x₁✝ x₂✝ : ↥↑↑I
h : (↑ℤ (↑↑I).subtype) x₁✝ = (↑ℤ (↑↑I).subtype) x₂✝
⊢ 1 • x₁✝ = 1 • x₂✝

Tactic:
rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]

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₁✝ x₂✝ : ↥↑↑I
h : (↑ℤ (↑↑I).subtype) x₁✝ = (↑ℤ (↑↑I).subtype) x₂✝
⊢ 1 • x₁✝ = 1 • x₂✝

Tactic:
by rwa [one_smul, one_smul, ← (Submodule.injective_subtype I.1.coeToSubmodule).eq_iff]

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

Goal state before:
pp: case inl
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
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q) * (C w * c ^ r))).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q) * (C w * c ^ r))).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q) * (C w * c ^ r))).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
radical_mul habcp.isRelPrime,

Goal state after:
case inl
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
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
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_1, ‖x_1 x‖

Tactic:
rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]

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

Goal state before:
pp: case inr
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
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
| inr hw =>

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

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

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

Tactic:
· rw [add_rotate] at heq hineq
    rw [mul_rotate] at hineq
    apply flt_catalan_aux heq <;> assumption

Goal state after:
case refine_3
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
heq' : C v * b ^ q + C w * c ^ r + C u * a ^ p = 0
hca : IsCoprime c a
⊢ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
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
⊢ σ • mk w.embedding = mk w'.embedding

Tactic:
smul_mk,

Goal state after:
case h
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
⊢ mk (w.embedding.comp ↑σ.symm) = mk w'.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ σ • mk w.embedding = mk w'.embedding

Tactic:
smul_mk,

Goal state after:
case h
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 : conjugate (w.embedding.comp (algebraMap k K)) = w'.embedding.comp (algebraMap k K)
σ : Gal(K/k)
hσ : ((starRingEnd ℂ).comp w.embedding).comp ↑σ.symm = w'.embedding
⊢ mk (w.embedding.comp ↑σ.symm) = mk w'.embedding
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)
⊢ mk (w.embedding.comp (algebraMap k K)) = (σ • mk w.embedding).comap (algebraMap k K)

Tactic:
smul_mk,

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)
⊢ mk (w.embedding.comp (algebraMap k K)) = (mk (w.embedding.comp ↑σ.symm)).comap (algebraMap k K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
this : convexBodySum K B = {0}
⊢ volume (convexBodySum K B) = 0

Tactic:
rw [this, measure_singleton]

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

Goal state before:
pp: 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 - y‖ ≤ B + B

Tactic:
refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)

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

case refine_2
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
⊢ ‖y‖ ≤ B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : InfinitePlace K → ℝ≥0
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
h : minkowskiBound K I < volume (convexBodyLT K f)
⊢ ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), w a < ↑(f w)

Tactic:
by
  have h_fund := ZSpan.isAddFundamentalDomain' (fractionalIdealLatticeBasis K I) volume
  have : Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I))).toAddSubgroup := by
    change Countable (span ℤ (Set.range (fractionalIdealLatticeBasis K I)))
    infer_instance
  obtain ⟨⟨x, hx⟩, h_nz, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
    h_fund (convexBodyLT_neg_mem K f) (convexBodyLT_convex K f) h
  rw [mem_toAddSubgroup, mem_span_fractionalIdealLatticeBasis] at hx
  obtain ⟨a, ha, rfl⟩ := hx
  exact ⟨a, ha, by simpa using h_nz, (convexBodyLT_mem K f).mp h_mem⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (-↑(nrComplexPlaces K)) * ↑(sqrt ‖discr K‖₊) * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (↑(nrRealPlaces K) * -1) * (π ^ (↑(nrComplexPlaces K) * -1) * 2 ^ (-↑(nrComplexPlaces K) * -1)))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))

Tactic:
mul_neg_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2 ^ (-↑(nrComplexPlaces K)) * ↑(sqrt ‖discr K‖₊) * 2 ^ ↑(finrank ℚ K) *
      (↑(finrank ℚ K).factorial *
        (2 ^ (-↑(nrRealPlaces K)) * (π ^ (-↑(nrComplexPlaces K)) * 2 ^ (- -↑(nrComplexPlaces K))))) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π ^ (-↑(nrComplexPlaces K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (parallelepiped ⇑(stdBasis K)) = 1

Tactic:
← measure_congr (ZSpan.fundamentalDomain_ae_parallelepiped (stdBasis K) volume),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (ZSpan.fundamentalDomain (stdBasis K)) = 1