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

Goal state before:
pp: case e'_4
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ Fintype.card ι •
      ((Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) =
    Fintype.card ι • y * ?convert_5

Tactic:
smul_mul_assoc,

Goal state after:
case e'_4
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ Fintype.card ι •
      ((Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) =
    Fintype.card ι • (y * ?e'_4.y)

case e'_4.y
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ ℤ
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n)), Λ m =
    ∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q

Tactic:
rw [sum_biUnion <| by rw [pairwiseDisjoint_iff]; grind [Prime.pow_inj']]

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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
show 2 * k + 1 - i = (2 * k - i) + 1 by lia,

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i + 1) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ θ (x ^ (1 / ↑i)) ≤ log 4 * √x

Tactic:
apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))

Goal state after:
case h
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ log 4 * x ^ (1 / ↑i) ≤ log 4 * √x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑(r.num - r.num * r.den.gcdA p % ↑p * ↑r.den) = 0

Tactic:
simp only [Int.cast_natCast, Int.cast_mul, Int.cast_sub]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃! n, n < p ∧ x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x
  use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_
  have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm
  rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
⊢ OfNat.ofNat n = ↑(OfNat.ofNat n)

Tactic:
rcases n with _ | _ | n <;> simp

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ∀ (x y : ℤ_[p]), ↑(f (x * y)) = ↑(f x) * ↑(f y)

Tactic:
by
    intro x y
    rw [f_congr (x * y) _ (f x * f y), cast_mul]
    · exact f_spec _
    · let I : Ideal ℤ_[p] := Ideal.span {↑v}
      convert! I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1
      rw [cast_mul]
      ring

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ ContinuousWithinAt (fun x ↦ -x⁻¹ / log x ^ 2) (Set.Icc 2 x) z

Tactic:
have : log z ^ 2 ≠ 0 := by
      refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> linarith

Goal state after:
case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this✝ : z ≠ 0
this : log z ^ 2 ≠ 0
⊢ ContinuousWithinAt (fun x ↦ -x⁻¹ / log x ^ 2) (Set.Icc 2 x) z
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } * star { re := x, im := y } = 1

Tactic:
simp [Zsqrtd.ext_iff, IsPell, mul_comm]

Goal state after:
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
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
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Tactic:
have t := mul_le_mul_of_nonneg_right h am1p

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
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 (n + 1) * { re := ↑a, im := -1 }
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ { re := re, im := im }.re.gcd { re := re, im := im }.im = 1

Tactic:
H1

Goal state after:
case refine_2
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ 1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.refine_1
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)
h : ↑p ^ p ^ k = 0
⊢ False

Tactic:
have := hne.1
      rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by lia)] at this
      exact absurd (eq_zero_of_pow_eq_zero h) this

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)

Tactic:
ext <;> simp [dz_val, az]

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n)) * ↑a + (↑a * ↑a - 1) * (↑(xn a1 n) + ↑(yn a1 n) * ↑a) + ↑(xn a1 n) =
    2 * ↑a * (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n))

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n) + (↑(xn a1 n) + ↑(yn a1 n) * ↑a) * ↑a + ↑(yn a1 n) =
    2 * ↑a * (↑(xn a1 n) + ↑(yn a1 n) * ↑a)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inr.inr.inl.refine_1
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x

pp: case inr.inr.inl.refine_2
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w

Tactic:
· dsimp only at h
      exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))

Goal state after:
case inr.inr.inl.refine_2
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ y ≤ y + w
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : k + 1 = 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))

Tactic:
add_eq_right

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : k = 0
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
rw [calc
          (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]
    exact
        nonnegg_neg_pos.2 (sqLe_mul.right.right.left (nonnegg_pos_neg.1 ha) (nonnegg_neg_pos.1 hb))

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 : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ ↑u' + 1 ≤ ↑v

Tactic:
exact mod_cast huv

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

Goal state before:
pp: case h.inl
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ - ↑u / ↑↑v| < (↑↑v * (2 * ↑↑v - 1))⁻¹
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul,
      cast_zero, inv_zero] at h

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

Goal state before:
pp: case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < ↑s
⊢ LSeriesSummable (logMul f) ↑s

pp: case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ LSeriesSummable f ↑s

Tactic:
· exact LSeriesSummable_logMul_of_lt_re <| by simp [hs]

Goal state after:
case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ LSeriesSummable f ↑s
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * ↑(x⁻¹ ^ P.k)) = 1

Tactic:
inv_rpow hx.le,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * ↑(x ^ P.k)⁻¹) = 1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: c d : ℝ
hcd : c ≤ d
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖x⁻¹ ^ (-(r + P.k))‖ / (‖P.ε⁻¹‖ * ‖x ^ P.k‖)

Tactic:
inv_rpow hx.le,

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(x ^ (-(r + P.k)))⁻¹‖ / (‖P.ε⁻¹‖ * ‖x ^ P.k‖)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
h : a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 0 x - 1‖ ≤ rexp (-π * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : 0 ≤ a
h : a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, ‖F_nat 0 a x‖ ≤ rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
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.ε * ↑(x⁻¹ ^ P.k)⁻¹) • P.g₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k)) • P.g₀

Tactic:
inv_rpow hx.le,

Goal state after:
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.ε * ↑(x ^ P.k)⁻¹⁻¹) • P.g₀ = (P.ε * ↑(x ^ P.k)) • P.g x - (P.ε * ↑(x ^ P.k)) • P.g₀
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t ↦
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop,
    ‖F_nat 1 a x‖ ≤
      rexp (-π * (a ^ 2 + 1) * x) / (1 - rexp (-π * x)) ^ 2 + a * rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : 0 ≤ a
this :
  ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)
p : ℝ
hp : 0 < p
hp' :
  (fun t ↦
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
    fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-π * (a ^ 2 + 1) * x)‖ ≤ rexp (-(π * a ^ 2) * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * (a ^ 2 + 1) * t)‖ ≤ rexp (-(π * a ^ 2) * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
⊢ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t) =O[atTop] fun t ↦ rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_int 0 (↑a) t - if a = 0 then 1 else 0) = (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
⊢ F_int 1 ↑a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : F_nat 1 (1 - a) =O[atTop] fun t ↦ rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ F_int 1 (↑a) t = F_nat 1 a t + F_nat 1 (1 - a) t
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ 0 ∨ P.f₀ = 0
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
⊢ DifferentiableAt ℂ P.Λ s

Tactic:
refine ((P.differentiable_Λ₀ s).sub ?_).sub ?_
  · rcases hs with hs | hs
    · fun_prop
    · simp [hs]
  · rcases hs' with hs' | hs'
    · fun_prop (disch := grind)
    · simp [hs']

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

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

Tactic:
refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂_term, mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ),
    exp_int_mul_two_pi_mul_I, mul_one]

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

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

pp: case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
· simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]

Goal state after:
case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖cosKernel (↑a) x - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 x - if 1 = 0 then 1 else 0)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖cosKernel (↑a) t - 1‖ ≤ 2 * (HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ((fun x ↦ χ ↑x) * f ⍟ ((fun x ↦ χ ↑x) * g)) n = ((fun x ↦ χ ↑x) * (f ⍟ g)) n

Tactic:
simp only [Pi.mul_apply, LSeries.convolution_def, Finset.mul_sum]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n✝ : ℕ
χ : DirichletCharacter R n✝
f g : ℕ → R
n : ℕ
⊢ ∑ x ∈ n.divisorsAntidiagonal, χ ↑x.1 * f x.1 * (χ ↑x.2 * g x.2) = ∑ i ∈ n.divisorsAntidiagonal, χ ↑n * (f i.1 * g i.2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖oddKernel (↑b) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) x

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖oddKernel (↑b) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) t
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖sinKernel (↑a) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs : s ≠ 0
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
refine (claim s hs hs').congr_of_eventuallyEq ?_
    filter_upwards [isOpen_compl_singleton.mem_nhds hs] with x hx
    simp [Function.update_of_ne hx]

Goal state after: