mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: 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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • B.basis.equivFun z i
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]

Tactic:
Basis.equivFun_apply

Goal state after:
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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: 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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

Tactic:
← H,

Goal state after:
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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z
i : Fin B.dim
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mpr
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ ↑z ∣ a

Tactic:
use ⟨r, i⟩

Goal state after:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rcases lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin | ein

Goal state after:
case refl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

case refl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |ξ * ↑k - ↑j| * |↑n + 1| ≤ 1

Tactic:
← abs_mul

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j + 4 * n * (q + 1)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
rw [Nat.mul_succ, ← add_assoc, add_comm]
      exact (xn_modEq_x4n_add _ _ _).trans IH

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ u v s t b,
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
refine ⟨a1,
        (Nat.eq_zero_or_pos k).elim (fun k0 => by rw [k0]; exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩)
          fun kpos => ?_⟩

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
kpos : k > 0
⊢ k ≤ yn a1 k ∧
    (xn a1 k = 1 ∧ yn a1 k = 0 ∨
      ∃ u v s t b,
        xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 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 k] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
n : ℕ
⊢ (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

Tactic:
by
  have h₀ : (n.primeFactorsList.filter (· ∈ s)).prod ≠ 0 :=
    List.prod_ne_zero fun h ↦ (pos_of_mem_primeFactorsList (List.mem_of_mem_filter h)).false
  refine ⟨h₀, fun p hp ↦ ?_⟩
  obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp
  simpa only [decide_eq_true_eq] using List.of_mem_filter <| mem_list_primes_of_dvd_prod H₁.prime
    (fun _ hq ↦ (prime_of_mem_primeFactorsList (List.mem_of_mem_filter hq)).prime) H₂

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(N.smoothNumbersUpTo k) + #(N.roughNumbersUpTo k) = N

Tactic:
by
  rw [smoothNumbersUpTo, roughNumbersUpTo,
    ← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
    Finset.filter_union_right]
  suffices #{x ∈ Finset.range (N + 1) | x ≠ 0} = N by
    have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
      have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
      refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
      simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
    rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]
  rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]
  simp only [Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
⊢ IsCoprime (u + -⌊ξ⌋ * v) v

Tactic:
IsCoprime.add_mul_right_left_iff

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
⊢ IsCoprime u v
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp

Goal state after:
case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
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 : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| = |(fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)|

Tactic:
rw [abs_sub_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
this :
  Tendsto (fun n ↦ ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime (u + -⌊ξ⌋ * v) v

Tactic:
IsCoprime.add_mul_right_left_iff

Goal state after:
case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
⊢ ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖

Tactic:
intro p hp

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n ↦ ‖f (p ^ n)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: c d : ℝ
hcd : c ≤ d
t : ℝ
⊢ 0 < t → ‖rexp (-d * t)‖ ≤ rexp (-c * t)

Tactic:
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 refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ (-P.k)

Tactic:
rw [← isBigO_norm_norm]
    simp_rw [mul_smul, norm_smul, mul_comm _ ‖P.g₀‖, ← mul_assoc, norm_real]
    apply (isBigO_refl _ _).const_mul_left

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

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
h : a = 0
t : ℝ
⊢ 0 < t → ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
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
t : ℝ
⊢ 0 < t → ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

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

Goal state before:
pp: case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2

pp: case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2

Tactic:
· simp_rw [hns, norm_mul, ← ofReal_ofNat, ← ofReal_intCast,
      norm_real, norm_of_nonneg zero_le_two, Real.norm_of_nonneg pi_pos.le, norm_I, mul_one,
      Real.norm_eq_abs, ← Int.cast_abs, ← Int.cast_pow]
    grw [ContinuousLinearMap.norm_fst_le, mul_one, ← Int.le_self_sq]

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ P.f_modif (1 / 1) = (P.ε * ↑(1 ^ P.k)) • P.g_modif 1

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
· simp [f_modif, g_modif]

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
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)
t : ℝ
⊢ 0 < t →
    ‖F_nat 1 a t‖ ≤
      rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
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: a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
⊢ 0 < t → ‖rexp (-π * (a ^ 2 + 1) * t)‖ ≤ rexp (-(π * a ^ 2) * t)

Tactic:
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.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' : x < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

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

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

Tactic:
· simp_rw [indicator_of_notMem (notMem_Ioi.mpr hx'.le), indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]
    abel

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

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

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

Tactic:
have (i : _) : ‖a i‖ / ↑(π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re := by
      rcases hq i with h | h
      · simp [h]
      · rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
    simpa only [this, mul_div_assoc] using h_sum.mul_left _

Goal state after:
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)
t : ℝ
⊢ 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

Tactic:
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)
t : ℝ
⊢ 0 < t → F_int 1 (↑a) t = F_nat 1 a t + F_nat 1 (1 - a) t

Tactic:
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
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (x : ℝ) in 0..1, ↑x ^ (s - 1)) * 1 = 1 / s * 1

Tactic:
simp [integral_cpow (.inl h_re1), zero_cpow (show s ≠ 0 by grind [P.hk, zero_re])]

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

Goal state before:
pp: ⊢ evenKernel 0 = cosKernel 0

Tactic:
by
  ext1 x
  simp [← QuotientAddGroup.mk_zero, ← ofReal_inj, evenKernel_def, cosKernel_def]

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

Goal state before:
pp: case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ ↑(cosKernel (↑a') x)) (Ioi 0)

Tactic:
simp only [cosKernel_def]

Goal state after:
case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ jacobiTheta₂ (↑a') (I * ↑x)) (Ioi 0)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
rw [(by simp : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • P.f₀))]

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 ((↑P.k - ↑P.k) • (1 / ↑P.k) • P.f₀))