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

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
⊢ List.Forall (fun S ↦ v ∈ S) (S :: l) ↔
    ∃ t,
      List.Forall (fun p ↦ p (v ⊗ t) = 0)
        (Poly.map (inl ⊗ inr ∘ inl) p :: List.map (fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl)

Tactic:
simpa using
        Iff.trans (and_congr (pe v) (ple v))
          ⟨fun ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ =>
            ⟨m ⊗ n, by
              rw [show (v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl) = v ⊗ m from
                    funext fun s => by rcases s with a | b <;> rfl]; exact hm, by
              refine List.Forall.imp (fun q hq => ?_) hn; dsimp [Function.comp_def]
              rw [show
                    (fun x : α ⊕ γ => (v ⊗ m ⊗ n) ((inl ⊗ fun x : γ => inr (inr x)) x)) = v ⊗ n
                    from funext fun s => by rcases s with a | b <;> rfl]; exact hq⟩,
            fun ⟨t, hl, hr⟩ =>
            ⟨⟨t ∘ inl, by
                rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl⟩,
              ⟨t ∘ inr, by
                refine List.Forall.imp (fun q hq => ?_) hr; dsimp [Function.comp_def] at hq
                rwa [show
                    (fun x : α ⊕ γ => (v ⊗ t) ((inl ⊗ fun x : γ => inr (inr x)) x)) =
                      v ⊗ t ∘ inr
                    from funext fun s => by rcases s with a | b <;> rfl] at hq ⟩⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
rcases s with a | b <;> try { cases a <;> rfl}; rfl

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩

Goal state after:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q ∈ insert p s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ p.succ.smoothNumbers

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩

Goal state after:
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q < p.succ
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x

Tactic:
exact ⟨or_iff_not_imp_left.2 fun h => mod_lt _ (Nat.pos_of_ne_zero h), x / y,
                  mod_add_div _ _⟩

Goal state after:
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
hp' : p ∉ {p ∈ s | Nat.Prime p}
⊢ HasSum (fun x ↦ f (p ^ x.1) * f ↑x.2) ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))

Tactic:
have : T3Space R := instT3Space

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}
this : T3Space R
⊢ HasSum (fun x ↦ f (p ^ x.1) * f ↑x.2) ((∑' (n : ℕ), f (p ^ n)) * ∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))
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
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ ∀ ε > 0,
    ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
intro ε hε

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
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (f ⍟ g) n / ↑n ^ s = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
convolution_def,

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (fun n ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2) n / ↑n ^ s =
    ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
use 0
      rw [convergent_zero, Rat.intCast_inj, eq_comm, floor_eq_iff]
      convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2) <;> norm_num

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

Goal state before:
pp: case h.inr.inl.inr.inl
ξ : ℝ
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₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)

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

Goal state before:
pp: case e'_5.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * ↑(rexp (-p i * t)) = (1 / ↑(p i)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / ↑(p i) ^ s) = a i * ((↑(p i) ^ s)⁻¹ * Complex.Gamma s)

Tactic:
div_eq_inv_mul

Goal state after:
case e'_5.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * ↑(rexp (-p i * t)) = (1 / ↑(p i)) ^ s * Complex.Gamma s
⊢ a i * ((↑(p i) ^ s)⁻¹ * Complex.Gamma s) = a i * ((↑(p i) ^ s)⁻¹ * Complex.Gamma s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ g_nat 0 a t = fun i ↦ rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ g_nat 0 a t n = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re

Tactic:
rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]

Goal state after:
case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ∫ (x : ℝ) in Ioi 0, ‖↑x ^ (s - 1) * ↑(rexp (-p i * x))‖ ∂volume = ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ (fun b ↦ ↑b * rexp (-π * (↑b + a ^ 2) * t)) = fun i ↦ rexp (-π * a ^ 2 * t) * (↑i * rexp (-π * t) ^ i)

Tactic:
ext1 n

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * (↑n * rexp (-π * t) ^ n)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ (fun b ↦ a * rexp (-π * (↑b + a ^ 2) * t)) = fun i ↦ a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i

Tactic:
ext1 n

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ EqOn (fun x ↦ P.f_modif x - P.f x + P.f₀)
    (((Ioo 0 1).indicator fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x ↦ P.f₀ - P.f 1) (Ioi 0)

Tactic:
intro x

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
⊢ x ∈ Ioi 0 →
    (fun x ↦ P.f_modif x - P.f x + P.f₀) x =
      (((Ioo 0 1).indicator fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
⊢ Summable fun a_1 ↦ ‖f_int k a t a_1‖

Tactic:
suffices ∀ n, ‖f_int k a t n‖ = ‖(Int.rec (f_nat k a t) (f_nat k (1 - a) t) : ℤ → ℝ) n‖ from
    funext this ▸ (HasSum.int_rec (summable_f_nat k a ht).hasSum
      (summable_f_nat k (1 - a) ht).hasSum).summable.norm

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ), ‖f_int k a t n‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
div_I,

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

Goal state before:
pp: case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u ↦ (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Tactic:
apply ContinuousAt.add

Goal state after:
case H.refine_2.hf
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u ↦ (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I)) x

case hg
a x : ℝ
hx : x ∈ Ioi 0
hf : Continuous fun u ↦ (↑a * I * ↑u, I * ↑u)
⊢ ContinuousAt (fun x ↦ ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) x
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: case e'_5
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ (fun n ↦ 1 / (↑n + ↑a) ^ s) = fun b ↦
    (1 / (↑b + ↑a) ^ s + 1 / (↑b + 1 - ↑a) ^ s) / 2 + (1 / (↑b + ↑a) ^ s - 1 / (↑b + 1 - ↑a) ^ s) / 2

Tactic:
ext1 n

Goal state after:
case e'_5
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 + (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
| (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)

Tactic:
2,

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
| fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) (expZeta (↑a) s)

Tactic:
convert! (hasSum_nat_cosZeta a hs).add ((hasSum_nat_sinZeta a hs).mul_left I) using 1

Goal state after:
case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) = fun b ↦
    ↑(Real.cos (2 * π * a * ↑b)) / ↑b ^ s + I * (↑(Real.sin (2 * π * a * ↑b)) / ↑b ^ s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s) = fun b ↦
    ↑(Real.cos (2 * π * a * ↑b)) / ↑b ^ s + I * (↑(Real.sin (2 * π * a * ↑b)) / ↑b ^ s)

Tactic:
ext1 n

Goal state after:
case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s =
    ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s + I * (↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2) * (cexp (-↑π * (I * z ^ 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ))) z =
    1 / (-I * τ) ^ (1 / 2) * deriv (fun z ↦ cexp (-↑π * (I * z ^ 2) / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
deriv_const_mul_field

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

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

Tactic:
eq_div_iff h3,

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t)) / (-2 * ↑π)

Tactic:
ofReal_exp,

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * cexp ↑(-π * ↑n ^ 2 * t) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t)) / (-2 * ↑π)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_1
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
⊢ Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re

Tactic:
apply (((summable_one_div_int_add_rpow 0 s.re).mpr hs).div_const 2).of_norm_bounded

Goal state after:
case refine_1
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
⊢ ∀ (i : ℤ), ‖‖c i‖ / |↑i| ^ s.re‖ ≤ 1 / |↑i + 0| ^ s.re / 2
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: case inl
χ : DirichletCharacter ℂ 0
⊢ 0 = δ 0

Tactic:
delta,

Goal state after:
case inl
χ : DirichletCharacter ℂ 0
⊢ 0 = if 0 = 1 then 1 else 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
by simp [← ofReal_mul, oddKernel_functional_equation a, inv_rpow (le_of_lt hx)]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 (if a = 0 then -1 * 2⁻¹ else 0)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
← div_eq_mul_inv

Goal state after:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ (Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0))
    s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (hurwitzOddFEPair a).Λ (↑(hurwitzOddFEPair ?m.63).k - (s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2

pp: a : UnitAddCircle
s : ℂ
⊢ UnitAddCircle

Tactic:
(hurwitzOddFEPair a).functional_equation ((s + 1) / 2),

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
| DifferentiableAt ℂ
    (fun s ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))) 1

Tactic:
2,

Goal state after:
a : UnitAddCircle
| fun s ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (1 / (1 - s) + 1 / (s - 1))

Tactic:
← neg_sub,

Goal state after:
a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (1 / -(s - 1) + 1 / (s - 1))
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : a ^ n = 1 ∨ a ^ n = -1
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rcases ha with ha | ha <;> rcases hb with hb | hb

Goal state after:
case neg.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

case neg.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r ^ 2 + s ^ 2) r

Tactic:
rw [sq, sq]

Goal state after:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
⊢ (↑(primeFactors a)).Pairwise IsRelPrime

Tactic:
intro x

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
⊢ x ∈ ↑(primeFactors a) → ∀ ⦃y : M⦄, y ∈ ↑(primeFactors a) → x ≠ y → IsRelPrime x y
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case 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)
hpn : p ∣ n.natAbs
⊢ False

Tactic:
rw [Int.gcd_comm] at hnp

Goal state after:
case 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 ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val.prod ∣ (normalizedFactors a).prod

Tactic:
apply Multiset.prod_dvd_prod_of_le

Goal state after:
case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val ≤ normalizedFactors a
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical (a * b) * divRadical c ∣ w

Tactic:
divRadical_mul hab

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ w
⊢ divRadical a * divRadical b * divRadical c ∣ w
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]

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

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical a * radical b * (divRadical a * divRadical b) = a * b

Tactic:
mul_mul_mul_comm,

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical a * divRadical a * (radical b * divRadical b) = a * b
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ (I.den * J.den) • ↑(I * J) = Submodule.map (Algebra.linearMap R K) (I.num * J.num)

Tactic:
have : Algebra.linearMap R K = (IsScalarTower.toAlgHom R R K).toLinearMap := rfl
        rw [coe_mul, this, Submodule.map_mul, ← this, ← den_mul_self_eq_num, ← den_mul_self_eq_num]
        exact Submodule.mul_smul_mul_eq_smul_mul_smul _ _ _ _

Goal state after: