mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε

Tactic:
obtain ⟨j, hj⟩ : ∃ j, ∀ i : Fin n,
      t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε := by
    by_contra! hg
    obtain ⟨j₀, j₁, j_ne, approx⟩ := exists_approx_polynomial hb hε
      (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
    revert j_ne approx
    refine Fin.cases ?_ (fun j₀ => ?_) j₀ <;>
      refine Fin.cases (fun j_ne approx => ?_) (fun j₁ j_ne approx => ?_) j₁
    · exact absurd rfl j_ne
    · rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
      have := (Classical.choose_spec (hg j₁)).2
      contradiction
    · rw [Fin.cons_succ, Fin.cons_zero, ← not_le] at approx
      have := (Classical.choose_spec (hg j₀)).2
      contradiction
    · rw [Fin.cons_succ, Fin.cons_succ] at approx
      rw [Ne, Fin.succ_inj] at j_ne
      have : j₀ = j₁ := (Classical.choose_spec (hg j₀)).1.symm.trans
        (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
          (Classical.choose_spec (hg j₁)).1)
      contradiction

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∑ i, #(Ioi i) = n * (n - 1) / 2

Tactic:
rw [← @Nat.cast_inj ℚ, Nat.cast_sum]

Goal state after:
case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∑ x, ↑(#(Ioi x)) = ↑(n * (n - 1) / 2)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ AddCommGroup (ℤ√d)

Tactic:
refine
  { sub := fun a b => a + -b
    nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
    zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩)
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    neg_add_cancel := ?_
    add_comm := ?_ } <;>
  intros

Goal state after:
case refine_1
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)

case refine_2
d : ℤ
a✝ : ℤ√d
⊢ 0 + a✝ = a✝

case refine_3
d : ℤ
a✝ : ℤ√d
⊢ a✝ + 0 = a✝

case refine_4
d : ℤ
a✝ : ℤ√d
⊢ -a✝ + a✝ = 0

case refine_5
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (-f)

Tactic:
by
  rw [← zero_sub]; exact (IsPoly.const 0).sub

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Tactic:
by
  injection pellZd_add a1 m n with _ h
  zify
  rw [h]
  simp [pellZd]

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

Goal state before:
pp: c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d

Tactic:
simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD yn a1 n ^ 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
      yn a1 n ^ 3]

Tactic:
exact ⟨L, R⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : i = 0
j2 : j = 2
⊢ False

Tactic:
rw [n1, j2] at j2n; exact absurd j2n (by decide)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ f.fn v hf ::ₒ v ∈ S

Tactic:
PFun.fn,

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (f v).get hf ::ₒ v ∈ S
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
rw [show x = x + 1 - 1 by ring] at h

Goal state after:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ x
⊢ abscissaOfAbsConv f ≤ ↑x + 1

Tactic:
rw [show x = x + 1 - 1 by ring] at h

Goal state after:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
⊢ n ^ k = m

Tactic:
have nt : (↑(n ^ k) : ℤ) < 2 * xn hw1 j * n - n * n - 1 :=
      eq_pow_of_pell_lem hn0.ne' hk0.ne' hnka

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ n ^ k = m
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u : ℤ
v : ℕ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
induction v using Nat.strong_induction_on generalizing ξ u with

Goal state after:
case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < ↑s
⊢ abscissaOfAbsConv f < ↑(↑s).re

Tactic:
by simp [hs]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ abscissaOfAbsConv (logMul f) < ↑(↑s).re

Tactic:
by simp [hs]

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

Goal state before:
pp: case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
hz : z.im < 0
⊢ False

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero

Goal state after:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto ((fun x ↦ rexp (-(2 * π * ↑x * z.im))) ∘ fun a ↦ ↑a) atTop (𝓝 0)
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ 1 / ↑x ^ (1 / 2) = 1 / ↑x ^ ↑(1 / 2)

Tactic:
ofReal_div,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ 1 / ↑x ^ (1 / 2) = 1 / ↑x ^ (↑1 / ↑2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ 1 / ↑(x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) = ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))

Tactic:
ofReal_div,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ 1 / ↑(x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x)) = ↑1 / ↑(x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Tactic:
simpa [this] using hasSum_jacobiTheta₂_term _ (by simpa)

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(cosKernel (↑a) t)

Tactic:
rw [cosKernel_def a t]
  have (n : ℤ) : cexp (2 * π * I * a * n) * cexp (-(π * n ^ 2 * t)) =
      jacobiTheta₂_term n a (I * ↑t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    ring_nf
    simp [sub_eq_add_neg]
  simpa [this] using hasSum_jacobiTheta₂_term _ (by simpa)

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

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

Tactic:
rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
⊢ ↑(1 / x) = 1 / ↑x

Tactic:
ofReal_div,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
⊢ ↑1 / ↑x = 1 / ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ ↑(3 / 2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
ofReal_div,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ (↑3 / ↑2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedCosZeta₀ 0 s = completedHurwitzZetaEven₀ 0 s

Tactic:
completedHurwitzZetaEven₀,

Goal state after:
s : ℂ
⊢ completedCosZeta₀ 0 s = (hurwitzEvenFEPair 0).Λ₀ (s / 2) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Tactic:
completedHurwitzZetaEven₀,

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ ((1 - s) / 2) / 2 = completedCosZeta₀ a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

Tactic:
ofReal_div,

Goal state after:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑1 / ↑2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s =
    completedHurwitzZetaEven a s / s.Gammaℝ

Tactic:
Function.update_of_ne h'

Goal state after:
case inl
a : UnitAddCircle
s : ℂ
h : a ≠ 0 ∨ s ≠ 0
h' : s ≠ 0
⊢ completedHurwitzZetaEven a s / s.Gammaℝ = completedHurwitzZetaEven a s / s.Gammaℝ
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑0 ^ (-s) = 0

Tactic:
by simp [hs]

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

Goal state before:
pp: s : ℂ
n : ℕ
χ : DirichletCharacter ℂ n
hs : s ≠ 0
⊢ χ ↑0 * ↑0 ^ (-s) = 0

Tactic:
by simp [hs]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
        (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n) / ↑n ^ s / 2)
    (completedSinZeta (↑a) s)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)

Tactic:
← add_div

Goal state after:
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)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ℤ
⊢ ¬z * z % ↑4 = 2 % ↑4

Tactic:
← ZMod.intCast_eq_intCast_iff'

Goal state after:
z : ℤ
⊢ ¬↑(z * z) = ↑2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (hurwitzZetaOdd (↑a) s)

Tactic:
refine ((hasSum_int_completedHurwitzZetaOdd a hs).div_const (Gammaℝ _)).congr_fun fun n ↦ ?_
  have : 0 < re (s + 1) := by rw [add_re, one_re]; positivity
  simp [div_right_comm _ _ (Gammaℝ _), mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)

Tactic:
← div_eq_mul_inv,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedSinZeta a s / (s + 1).Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)

Tactic:
← div_eq_mul_inv,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) / (s + 1).Gammaℝ) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * (completedHurwitzZetaOdd a s / (s + 1).Gammaℝ)
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 ∣ derivative b

Tactic:
apply hc.symm.dvd_of_dvd_mul_left

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 ∣ a * derivative b
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a.wronskian b = 0
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
rw [wronskian, sub_eq_iff_eq_add, zero_add] at hw
    constructor
    · rw [← dvd_derivative_iff]
      apply hc.dvd_of_dvd_mul_right
      rw [← hw]; exact dvd_mul_right _ _
    · rw [← dvd_derivative_iff]
      apply hc.symm.dvd_of_dvd_mul_left
      rw [hw]; exact dvd_mul_left _ _

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 (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬p ∣ 1

Tactic:
exact mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m = m0 * 2 + 1
n0 : ℤ
hn2 : n = n0 * 2 + 1
⊢ 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

Tactic:
subst m

Goal state after:
n : ℤ
hn : n % 2 = 1
m0 n0 : ℤ
hn2 : n = n0 * 2 + 1
h : (m0 * 2 + 1).gcd n = 1
hm : (m0 * 2 + 1) % 2 = 1
⊢ 2 ∣ (m0 * 2 + 1) ^ 2 + n ^ 2 ∧
    2 ∣ (m0 * 2 + 1) ^ 2 - n ^ 2 ∧
      ((m0 * 2 + 1) ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ (((m0 * 2 + 1) ^ 2 - n ^ 2) / 2).gcd (((m0 * 2 + 1) ^ 2 + n ^ 2) / 2) = 1
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ primeFactors 1 = ∅

Tactic:
primeFactors_one

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ ∅ = ∅
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

Tactic:
classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]

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
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
by
  set w := wronskian a b with wab
  have hbc : IsCoprime b c := by
    rw [add_eq_zero_iff_neg_eq] at hsum
    rw [← hsum, IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hab.symm 1
    rw [mul_one]
  have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
  have hca : IsCoprime c a := by
    rw [add_eq_zero_iff_neg_eq] at hsum'
    rw [← hsum', IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hbc.symm 1
    rw [mul_one]
  have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
  have wca : w = wronskian c a := by
    rw [add_rotate] at hsum
    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
  -- have `divRadical x` dividing `w` for `x = a, b, c`, and use coprimality
  have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
    have adr_dvd_w := divRadical_dvd_wronskian_left a b
    have bdr_dvd_w := divRadical_dvd_wronskian_right a b
    have cdr_dvd_w := divRadical_dvd_wronskian_right b c
    rw [← wab] at adr_dvd_w bdr_dvd_w
    rw [← wbc] at cdr_dvd_w
    rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
    exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
  by_cases hw : w = 0
  · right
    rw [hw] at wab wbc
    obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm
    obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm
    exact ⟨ga, gb, gc⟩
  · left
    -- use `abc_subcall` three times, using the symmetry in `a, b, c`
    refine ⟨?_, ?_, ?_⟩
    · rw [mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wbc <;> assumption
    · rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption
    · apply abc_subcall wab <;> assumption

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ (⟨↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a, ⋯⟩, ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩).2 • x =
    (↑ℤ (↑↑I).subtype) (⟨↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a, ⋯⟩, ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩).1

Tactic:
simp_rw [LinearMap.coe_restrictScalars, Submodule.coe_subtype] at h ⊢

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h : x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d) = (algebraMap (𝓞 K) K) a
⊢ ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩ • x = ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a