mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2.refine_1
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ (out x).snd ∈ ↑((Substructure.closure L).toFun (Classical.choose ⋯))

pp: case refine_2.refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ (of L ι G f (out x).fst).toHom (out x).snd = x

Tactic:
· rw [(Classical.choose_spec (h (out x).1).out).2]
      trivial

Goal state after:
case refine_2.refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ (of L ι G f (out x).fst).toHom (out x).snd = x
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
⊢ (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ≃[L] ↥(iSup ⇑S)

Tactic:
let F := Embedding.codRestrict (⨆ i, S i) _ liftInclusion_in_sup

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
liftInclusion_in_sup :
  ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯), (liftInclusion S) x ∈ ⨆ i, S i
F : (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ↪[L] ↥(⨆ i, S i) :=
  Embedding.codRestrict (⨆ i, S i) (liftInclusion S) liftInclusion_in_sup
⊢ (DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯) ≃[L] ↥(iSup ⇑S)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ (x✝ ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + (fromCols 1 0).fromCols 1 *ᵥ x✝

Tactic:
simp [fromCols_mulVec]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
this : Fintype ι
x✝ : (ι ⊕ ι) ⊕ ι → ℕ
⊢ i + (x✝ ∘ Sum.inl) ∘ Sum.inr = i + (fromCols 0 1).fromCols 0 *ᵥ x✝

Tactic:
simp [fromCols_mulVec]

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
rw [ha]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (v * a) ^ 2 * x ^ 2 * (v * a * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * (v * a) * (v * (a * x ^ 2 * ((v * a * x) ^ (i - 2) * ↑(p.choose i / p))))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
by_cases hnp : n = p ^ n.factorization p

Goal state after:
case pos
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

case neg
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))

Tactic:
coeff_subst' hg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff (n + 1)) (g ^ d) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 2 n)

Tactic:
simp +contextual [primesBelow_eq_filter_range, Nat.Prime.two_le]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ (vonStaudtPrimes k).erase p, 1 / ↑q

Tactic:
have hp_mem : p ∈ vonStaudtPrimes k := Finset.mem_filter.mpr
      ⟨Finset.mem_range.mpr (by have := Nat.le_of_dvd (by lia) hdvd; lia), Fact.out, hdvd⟩
    rw [← Finset.add_sum_erase _ _ hp_mem]
    simp [vonStaudtIndicator, hdvd]

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
refine coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).degree < b.degree
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den

Tactic:
by
  induction k using Nat.strong_induction_on with
  | _ k ih =>
    obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk
    rw [hT]
    have hT_int : pIntegral p T := Int.padicValuation_le_one p T
    have hR := pIntegral_faulhaber_sum hk fun m hm_pos hm_lt ↦
      Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)
    exact Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b

Tactic:
have := dvd_add ha hb

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val <
    p.sub 0

Tactic:
apply ZMod.val_lt

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ ContinuousAt (fun x ↦ 1 / log x ^ 2) x

Tactic:
have : x ≠ 0 := by grind

Goal state after:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ ContinuousAt (fun x ↦ 1 / log x ^ 2) x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ ↑(π ⌊x⌋₊)

Tactic:
grw [div_le_iff₀ (log_pos hx), ← psi_le_primeCounting_mul_log', psi_ge']

Goal state after:
case hx
x : ℝ
hx : 1 < x
⊢ 0 ≤ x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ ↑(p ^ k) ∣ nthHom f r j - nthHom f r k

Tactic:
exact mod_cast pow_dvd_nthHom_sub f_compat r k j hj

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 1 * x✝ = x✝

Tactic:
by ext; rw [mul_apply, one_apply, one_mul]

Goal state after:
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 (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H

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 (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
⊢ (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: d : ℕ
a b : ℤ√↑d
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
have ht : b ≤ a ∨ a ≤ b := by
      have t := (a - b).nonneg_total
      rwa [neg_sub] at t

Goal state after:
d : ℕ
a b : ℤ√↑d
ht : b ≤ a ∨ a ≤ b
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ 2 * n ≤ n + j

Tactic:
two_mul

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ 2 * n

Tactic:
two_mul

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n
Module: Mathlib.NumberTheory.LSeries.Deriv

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

Tactic:
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:
simp [hs]

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

Goal state before:
pp: ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ

Tactic:
refine ⟨(fract_lt_one ξ).le, ?_⟩

Goal state after:
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ 2⁻¹ < fract ξ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: c d : ℝ
hcd : c ≤ d
⊢ (fun t ↦ rexp (-d * t)) =O[atTop] fun t ↦ rexp (-c * t)

Tactic:
apply Eventually.isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [norm_of_nonneg (exp_pos _).le]
  gcongr

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

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (2 * ↑i) ^ k

Tactic:
two_mul

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (↑i + ↑i) ^ k
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ P.f x - P.f₀) =O[𝓝[>] 0] fun x ↦ x ^ (-P.k)

Tactic:
by
  simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]
  refine (P.hf_zero _).add (IsBigO.sub ?_ ?_)
  · rw [← isBigO_norm_norm]
    simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]
    apply (isBigO_refl _ _).const_mul_left
  · refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)
    filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)
    apply le_mul_of_one_le_right (norm_nonneg _)
    rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]
    exact (one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ ∀ (i : ℤ), ‖f i (z, τ)‖ ≤ ↑|i| ^ 0 * rexp (-π * (T * ↑i ^ 2 - 2 * S * ↑|i|))

Tactic:
simpa only [pow_zero, one_mul] using! norm_jacobiTheta₂_term_le hT hz.le hτ'.le

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

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

Tactic:
simp [hs]

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

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

Tactic:
by
  simp_rw [Λ, smul_sub, (by simp : 𝓝 (-P.f₀) = 𝓝 (((0 : ℂ) • P.Λ₀ 0) - P.f₀ - 0))]
  refine ((Tendsto.mono_left ?_ nhdsWithin_le_nhds).sub ?_).sub ?_
  · exact (continuous_id.smul P.differentiable_Λ₀.continuous).tendsto _
  · refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
    filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
    match_scalars
    grind
  · rw [show 𝓝 0 = 𝓝 ((0 : ℂ) • (P.ε / (P.k - 0 : ℂ)) • P.g₀) by rw [zero_smul]]
    exact (continuousAt_id.smul ((continuousAt_const.div ((continuous_sub_left _).continuousAt)
      (by simpa using P.hk.ne')).smul continuousAt_const)).mono_left nhdsWithin_le_nhds

Goal state after:
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)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))

Tactic:
h3,

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)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / ↑(x ^ (1 / 2)) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (-1 / (I * ↑x))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂ z τ

Tactic:
conv_rhs => rw [jacobiTheta₂, ← tsum_mul_left, ← (Equiv.addRight 1).tsum_eq]

Goal state after:
z τ : ℂ
⊢ jacobiTheta₂ (z + τ) τ = ∑' (c : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) c) z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
← neg_inj,

Goal state after:
z τ : ℂ
⊢ -(starRingEnd ℂ) (jacobiTheta₂' z τ) = -jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
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 ↦ 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))
⊢ Summable fun i ↦ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re

Tactic:
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.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) *
      ∑' (x : ℤ), cexp (↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑x * (z / τ) + ↑π * I * ↑x ^ 2 * (-1 / τ)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ∈ Ioi 0
⊢ (ofReal ∘ evenKernel a) (1 / x) = (1 * ↑(x ^ (1 / 2))) • (ofReal ∘ cosKernel a) x

Tactic:
simp [← ofReal_mul, evenKernel_functional_equation, inv_rpow (le_of_lt hx)]

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

Goal state before:
pp: a b : UnitAddCircle
⊢ Differentiable ℂ fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s + (hurwitzZetaOdd a s - hurwitzZetaOdd b s)

Tactic:
refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)

Goal state after:
case refine_1
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd a)

case refine_2
a b : UnitAddCircle
⊢ Differentiable ℂ (hurwitzZetaOdd b)
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:
Summable.tsum_eq_zero_add

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.SumPrimeReciprocals

Goal state before:
pp: case h
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 : 1 / 2 ≤ S
⊢ (2 ^ 2) ^ (k.primesBelow.card + 1) = 2 * N₀

Tactic:
pow_right_comm

Goal state after:
case h
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 : 1 / 2 ≤ S
⊢ (2 ^ (k.primesBelow.card + 1)) ^ 2 = 2 * N₀
Module: Mathlib.NumberTheory.SumPrimeReciprocals

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

Tactic:
exact_mod_cast p.prop.one_lt.le

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_oddKernel a

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : oddKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

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

Tactic:
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:
simp [hs]

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

Goal state before:
pp: a b c : ℤ
⊢ Minimal a b c → Minimal a b (-c)

Tactic:
rintro ⟨⟨ha, hb, heq⟩, h2⟩
  constructor
  · apply And.intro ha (And.intro hb _)
    rw [heq]
    exact (neg_sq c).symm
  rwa [Int.natAbs_neg c]

Goal state after: