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

Goal state before:
pp: f : ℕ → ℝ
x : ℝ
h : (abscissaOfAbsConv fun x ↦ ↑(f x)) < ↑x
aux : term (fun x ↦ ↑(f x)) ↑x = fun n ↦ ↑(if n = 0 then 0 else f n / ↑n ^ x)
this : Summable fun x_1 ↦ if x_1 = 0 then 0 else f x_1 / ↑x_1 ^ x
n : ℕ
hn : n ∈ {0}ᶜ
⊢ ¬n = 0

Tactic:
by simpa using hn

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
hu'ℝ,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - (↑u' + ↑⌊ξ⌋ * ↑v) / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑⌊ξ⌋ - ↑u' / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
self_sub_floor,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < fract ξ - ↑u' / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f f' g g' : ℕ → R
hf : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
hg : ∀ {n : ℕ}, n ≠ 0 → g n = g' n
⊢ f ⍟ g = f' ⍟ g'

Tactic:
by
  simp [convolution, toArithmeticFunction_congr hf, toArithmeticFunction_congr hg]

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

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : ξ - ↑⌊ξ⌋ < (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v

Tactic:
self_sub_floor,

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * max 0 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
max_eq_right zero_le_one,

Goal state after:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * 1 ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))

Tactic:
simp_rw [mul_assoc (3 * π)]

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * (↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖) ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ P.f x - P.f₀ + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x - P.f x + P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
indicator_of_notMem (notMem_Ioo_of_ge hx'.le),

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ P.f x - P.f₀ + 0 - P.f x + P.f₀ = 0 + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s

Tactic:
rcases eq_or_ne (p i) 0 with h | h <;>
    simp [a', h, ofReal_zero, zero_cpow hs', div_zero]

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

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

Tactic:
mul_comm _ (n : ℂ),

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

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - 1 / s

Tactic:
WeakFEPair.symm,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.Λ₀
          (s / 2) /
        2 -
      (1 / (s / 2)) •
          { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.f₀ /
        2 =
    { f := (hurwitzEvenFEPair a).g, g := (hurwitzEvenFEPair a).f, k := (hurwitzEvenFEPair a).k,
              ε := (hurwitzEvenFEPair a).ε⁻¹, f₀ := (hurwitzEvenFEPair a).g₀, g₀ := (hurwitzEvenFEPair a).f₀,
              hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯, h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }.Λ₀
          (s / 2) /
        2 -
      1 / s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x))

Tactic:
rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
    mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]

Goal state after:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ ((hurwitzEvenFEPair a).symm.ε / (↑(hurwitzEvenFEPair a).symm.k - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)

Tactic:
WeakFEPair.symm,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ ((hurwitzEvenFEPair a).ε⁻¹ / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - ↑(1 / 2)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] ↑(1 / 2)) (𝓝 (1 * 1))
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [push_cast, one_mul] at h1

Goal state after:
a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: ⊢ (fun n ↦ 1 n) = δ

Tactic:
by
  ext
  simp [one_apply, LSeries.delta]

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

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))

Tactic:
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self two_ne_zero, one_mul,
    neg_mul, neg_mul, neg_neg, mul_comm _ I, ← mul_assoc, mul_comm _ I, neg_mul,
    ← sub_eq_neg_add, mul_sub]

Goal state after:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ I * ↑n * cexp (-(2 * ↑π * ↑a * ↑n * I)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
rcases h a b c ha hb hc heq with ⟨d, a', b', c', ⟨rfl, rfl, rfl⟩, ⟨ua, ub, uc⟩⟩

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
d a' b' c' : R
ha : a' * d ≠ 0
hb : b' * d ≠ 0
hc : c' * d ≠ 0
heq : (a' * d) ^ n + (b' * d) ^ n = (c' * d) ^ n
ua : IsUnit a'
ub : IsUnit b'
uc : IsUnit c'
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i ↦ 1 / |↑i| ^ s.re / 2

Tactic:
apply Summable.div_const

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i ↦ 1 / |↑i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

Tactic:
let c (n : ℤ) : ℂ := 1 / 2

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr.inr
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ (4 * (x0 * x0 + x0 + y0 * y0 + y0) + 2) % 4 = 2

Tactic:
simp only [Int.add_emod, Int.mul_emod_right, zero_add]

Goal state after:
case inr.inr
z x0 y0 : ℤ
hx : (x0 * 2 + 1) % 2 = 1
hy : (y0 * 2 + 1) % 2 = 1
h : PythagoreanTriple (x0 * 2 + 1) (y0 * 2 + 1) z
hc : (x0 * 2 + 1).gcd (y0 * 2 + 1) = 1
⊢ 2 % 4 % 4 = 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ IsCoprime a n

Tactic:
apply @IsCoprime.of_mul_left_left _ _ _ a

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ IsCoprime (a * a) n
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ a.wronskian a = 0

Tactic:
by
  rw [wronskian, mul_comm, sub_self]

Goal state after:
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
⊢ ↑p ∣ 2 * m ^ 2

Tactic:
convert! dvd_add hp2 hp1 using 1

Goal state after:
case e'_4
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
⊢ 2 * m ^ 2 = m ^ 2 + n ^ 2 + (m ^ 2 - n ^ 2)
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:
by
  rw [← eulerProduct_log_eq_LSeries χ hs, LSeries_eulerProduct_exp_log χ hs]

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 : ℕ
⊢ divRadical (p ^ (i + 1)) ∣ derivative (p ^ (i + 1))

Tactic:
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 : 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
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
⊢ divRadical (a * b * c) ∣ w

Tactic:
have adr_dvd_w := divRadical_dvd_wronskian_left a b

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 = 0
w : k[X] := a.wronskian b
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
adr_dvd_w : divRadical a ∣ a.wronskian b
⊢ divRadical (a * b * c) ∣ w
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
hc : IsRelPrime a b
⊢ radical (a * b) = radical a * radical b

Tactic:
by
  simp_rw [radical]
  rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ↔ ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsComplex → ¬ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case mpr
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✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r

Tactic:
rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩

Goal state after:
case mpr
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
hx1 : IsIntegral ℤ x
hx2 : ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
⊢ (canonicalEmbedding K) x ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r
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 : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ (w.comap f).IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff]

Goal state after:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
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
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ (w.comap ↑f).mult ≤ ((w.comap ↑f).comap (algebraMap k K)).mult

Tactic:
← InfinitePlace.comap_comp,

Goal state after:
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
inst✝ : Algebra k F
w : InfinitePlace F
h : IsUnramified k w
f : K →ₐ[k] F
⊢ (w.comap ↑f).mult ≤ (w.comap ((↑f).comp (algebraMap k K))).mult
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : ¬ComplexEmbedding.IsReal w₂.embedding ∧ (w₂.comap (algebraMap k K)).IsReal
h_eq : w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
exact Ne.symm (h_eq ▸ h.1)

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

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ ¬0 ≤ ↑(discr K)

Tactic:
Int.cast_nonneg_iff,

Goal state after:
case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ ¬0 ≤ discr 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
hw : ¬IsUnramifiedIn K w
⊢ Even (finrank k K)

Tactic:
by
  obtain ⟨v, rfl⟩ := comap_surjective (K := K) w
  rw [isUnramifiedIn_comap] at hw
  exact even_finrank_of_not_isUnramified hw

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖) =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K

Tactic:
by
        rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]
        simp_rw [norm_eq_abs]

Goal state after:
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)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT K f
⊢ a ≠ 0

Tactic:
by simpa using h_nz

Goal state after:
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)ˣ
w₀ : { w // w.IsComplex }
h : minkowskiBound K I < volume (convexBodyLT' K f w₀)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodyLT' K f w₀
⊢ a ≠ 0

Tactic:
by simpa using h_nz

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ a ≠ 0

Tactic:
by simpa using h_nz

Goal state after: