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
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case neg
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (if False then (trace K L) (z * B.gen ^ ↑(σ j)) else traceMatrix K (fun i ↦ B.gen ^ ↑i) (σ j) j) ∈ ⊥

Tactic:
exact mem_bot.2
      (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ 1 ≤ b * { re := ↑a, im := -1 }

Tactic:
← a1m

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ { re := ↑a, im := 1 } * { re := ↑a, im := -1 } ≤ b * { re := ↑a, im := -1 }
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * (Algebra.norm K) (ζ ^ p ^ k - 1) =
    (Algebra.norm K) (↑(p ^ (k + 1)) * ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
hnorm,

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    (Algebra.norm K) (↑(p ^ (k + 1)) * ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Tactic:
rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩

Goal state after:
case mpr
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case nonzero
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : re 0 = 0
him : im 0 = 0
⊢ False

Tactic:
simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑0, im := ↑(y + 1) } + { re := ofNat x, im := -[y+1] }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑0 } + { re := -[x+1], im := ofNat y }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑(y + 1) } + { re := -[x+1], im := -[y+1] }).Nonneg

Tactic:
simp [Int.negSucc_eq, add_assoc, Nonneg, Nonnegg]

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

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Tactic:
have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
  rw [this]
  exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)

Tactic:
apply dvd_mul_right

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

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : 0 * 0 = d * a.im * a.im
h : d < 0
this : a.re * a.re = 0
⊢ 0 = re 0 ∧ a.im = im 0

Tactic:
simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul,
        mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha

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

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
⊢ a.norm = 0 ↔ a = 0

Tactic:
refine ⟨fun ha => Zsqrtd.ext_iff.mpr ?_, fun h => by rw [h, norm_zero]⟩
  dsimp only [norm] at ha
  rw [sub_eq_zero] at ha
  by_cases! h : 0 ≤ d
  · obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
    have : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
    exact divides_sq_eq_zero_z ha
  · suffices a.re * a.re = 0 by
      rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
      simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul,
        mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha
    apply _root_.le_antisymm _ (mul_self_nonneg _)
    rw [ha, mul_assoc]
    exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
⊢ f = g

Tactic:
ext ⟨re_x, im_x⟩
  simp [decompose, h]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
⊢ p ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0

Tactic:
rw [show (v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ x) ⊗ t from
            funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl]

Goal state after:
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
⊢ p ((v ⊗ x) ⊗ t) = 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ q : ℚ
h : |ξ * ↑q.den - ↑q.num| < 1 / (↑q.den * ↑q.den) * ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den

Tactic:
div_mul,

Goal state after:
ξ q : ℚ
h : |ξ * ↑q.den - ↑q.num| < 1 / (↑q.den * ↑q.den / ↑q.den)
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
p : Poly α
v : Option α → ℕ
⊢ v ∈ {v | (fun v ↦ (p v).natAbs) (v ∘ some) = v none} ↔
    ((Poly.map some p - Poly.proj none) * (Poly.map some p + Poly.proj none)) v = 0

Tactic:
dsimp; exact Int.natAbs_eq_iff_mul_eq_zero

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
ipos : i > 0
this : i = k
⊢ xn a1 k = xn a1 i ∧ yn a1 k = yn a1 i

Tactic:
by rw [this]; exact ⟨rfl, rfl⟩

Goal state after:
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
  by_contra! H
  obtain ⟨y, hy₁, hy₂⟩ := EReal.exists_between_coe_real H
  exact (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
ipos : i > 0
⊢ xn a1 k = xn a1 i ∧ yn a1 k = yn a1 i

Tactic:
by
            suffices i = k by rw [this]; exact ⟨rfl, rfl⟩
            clear o rem xy uv st
            have iln : i ≤ n :=
              le_of_not_gt fun hin =>
                not_lt_of_ge (Nat.le_of_dvd vp (dvd_of_mul_left_dvd yv)) (strictMono_y a1 hin)
            have yd : 4 * yn a1 i ∣ 4 * n := by gcongr; exact dvd_of_ysq_dvd a1 yv
            have jk : j ≡ k [MOD 4 * yn a1 i] :=
              have : 4 * yn a1 i ∣ b - 1 :=
                Int.natCast_dvd_natCast.1 <| by rw [Int.ofNat_sub (le_of_lt b1)]; exact bm1.symm.dvd
              ((yn_modEq_a_sub_one b1 _).of_dvd this).symm.trans tk
            have ki : k + i < 4 * yn a1 i :=
              lt_of_le_of_lt (_root_.add_le_add ky (yn_ge_n a1 i)) <| by
                rw [← two_mul]
                exact Nat.mul_lt_mul_of_pos_right (by decide) (strictMono_y a1 ipos)
            have ji : j ≡ i [MOD 4 * n] :=
              have : xn a1 j ≡ xn a1 i [MOD xn a1 n] :=
                (xy_modEq_of_modEq b1 a1 ba j).left.symm.trans sx
              (modEq_of_xn_modEq a1 ipos iln this).resolve_right
                fun ji : j + i ≡ 0 [MOD 4 * n] =>
                not_le_of_gt ki <|
                  Nat.le_of_dvd (lt_of_lt_of_le ipos <| Nat.le_add_left _ _) <|
                    modEq_zero_iff_dvd.1 <| (jk.symm.add_right i).trans <| ji.of_dvd yd
            have : i % (4 * yn a1 i) = k % (4 * yn a1 i) := (ji.of_dvd yd).symm.trans jk
            rwa [Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_left _ _) ki),
              Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_right _ _) ki)] at this

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

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

Tactic:
replace h := (h.comp_injective this).tendsto_atTop_zero

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

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑((1 / x) ^ (-P.k))) • P.g₀ =
    (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k)) • P.g₀

Tactic:
simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • P.Λ₀ s - s • (1 / s) • P.f₀ - s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 (0 • P.Λ₀ 0 - P.f₀ - 0))

Tactic:
refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).sub ?_

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))

case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u ↦ (↑a * I * ↑u, I * ↑u)
⊢ 0 < (I * ↑x).im

Tactic:
I_mul_im,

Goal state after:
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u ↦ (↑a * I * ↑u, I * ↑u)
⊢ 0 < (↑x).re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < im ?m.76

Tactic:
I_mul_im,

Goal state after:
a x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < re ?m.80

a x : ℝ
hx : x ∈ Ioi 0
⊢ ℂ
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
⊢ HasSum (fun i ↦ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))

Tactic:
have hs₁ : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
  have hs₂ : 0 < (s + 1).re := by rw [add_re, one_re]; positivity
  have hs₃ : s + 1 ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs₂)
  have (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)) := by
    split_ifs with h <;> simp [h]
  conv at hF => enter [t, ht, 1, i]; rw [this]
  convert! hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 with i
  · rcases eq_or_ne (r i) 0 with h | h
    · rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]
    · rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]
      conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]
      field [h]
  · convert! h_sum using 2 with i
    rcases eq_or_ne (r i) 0 with h | h
    · rw [h, abs_zero, ofReal_zero, zero_rpow hs₂.ne', zero_rpow hs.ne', div_zero, div_zero]
    · rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr h)]

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

Goal state before:
pp: a x : ℝ
hx : 0 < x
⊢ 0 < im ?m.70

Tactic:
I_mul_im,

Goal state after:
a x : ℝ
hx : 0 < x
⊢ 0 < re ?m.74

a x : ℝ
hx : 0 < x
⊢ ℂ
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))
⊢ 0 < im ?m.87

Tactic:
I_mul_im,

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))
⊢ 0 < re ?m.91

a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
⊢ ℂ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ 0 < (I * ↑t).im

Tactic:
I_mul_im,

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ 0 < (↑t).re
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Tactic:
have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
    continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by simp_all)

Goal state after:
this : Tendsto (fun s ↦ ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)
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 * (2 * ↑m ^ 2) - ↑m * (2 * ↑m) ≤ 2 * (2 * ↑m ^ 2) * S
⊢ 1 / 2 ≤ S

Tactic:
show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,

Goal state after:
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 * (2 * ↑m ^ 2) * (1 / 2) ≤ 2 * (2 * ↑m ^ 2) * S
⊢ 1 / 2 ≤ S
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: r : ℝ
h : ¬r < -1
H : Summable fun p ↦ ↑↑p ^ r
p : Primes
⊢ 1 ≤ ↑↑p

Tactic:
by exact_mod_cast p.prop.one_lt.le

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs,

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
hs' : (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re
hΛ : LSeriesSummable ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s * L (fun n ↦ χ ↑n) s = -deriv (L fun n ↦ χ ↑n) s
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
n : ℤ
⊢ ‖cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2

Tactic:
norm_exp_ofReal_mul_I

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < z * z

Tactic:
← h.eq,

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x * x + y * y
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

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

Tactic:
simp only [div_eq_mul_inv _ (_ ^ _), ← cpow_neg]
      suffices (Function.support f) ⊆ {n | IsPrimePow n} from
        tsum_subtype_eq_of_support_subset this
      intro n hn
      contrapose! hn
      simp [f, vonMangoldt_eq_zero_iff.mpr hn]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.inr
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
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ ↑p ∣ n * n

Tactic:
rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]

Goal state after:
case inl.inr
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
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
hpm : p ∣ m.natAbs
⊢ ↑p ∣ -(m ^ 2 - n ^ 2) + m * m
Module: Mathlib.RingTheory.Radical.Basic

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

Tactic:
induction s using Finset.cons_induction with

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

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

Tactic:
induction s using Finset.cons_induction with

Goal state after: