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

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

Tactic:
map_mul,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ ((x✝³ + x✝²) * x✝¹) x✝ = (x✝³ * x✝¹ + x✝² * x✝¹) x✝

Tactic:
simp only [add_apply, mul_apply]

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ x✝ + x✝² x✝) * x✝¹ x✝ = x✝³ x✝ * x✝¹ x✝ + x✝² x✝ * x✝¹ x✝
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
yl2 :
  { re := { re := x, im := y }.re + (-{ re := x, im := -y }).re,
      im := { re := x, im := y }.im + (-{ re := x, im := -y }).im } <
    { re := { re := ↑a, im := 1 }.re + (-{ re := ↑a, im := -1 }).re,
      im := { re := ↑a, im := 1 }.im + (-{ re := ↑a, im := -1 }).im }
y0l : 0 < { re := 0, im := y + y }
⊢ False

Tactic:
simp only [Zsqrtd.re_neg, add_neg_cancel,
          Zsqrtd.im_neg, neg_neg] at yl2

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := 0, im := y + y }
yl2 : { re := 0, im := y + y } < { re := 0, im := 1 + 1 }
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD a - 1]

Tactic:
yn_succ_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ n + 2 + n [MOD a - 1]
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
yn_succ_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ n + 2 + n [MOD 2]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) (a * star a) = 0

Tactic:
map_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) a * (lift r) (star a) = 0
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
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd

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
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
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
k0 : 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])

Tactic:
by rw [k0]; exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩

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

Goal state before:
pp: ξ : ℝ
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ

Tactic:
refine
    ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ => ?_,
      Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩

Goal state after:
ξ : ℝ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite
a b : ℤ
x✝ : b ≠ 0
⊢ ξ ≠ ↑a / ↑b
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
⊢ False

Tactic:
cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2)

Goal state after:
case inl
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
h✝ : v = 1
⊢ False

case inr
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
h✝ : v = -1
⊢ False
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
this : List.filter (fun x ↦ decide (x = p)) m.primeFactorsList = List.filter (fun x ↦ decide (x ∉ s)) m.primeFactorsList
⊢ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ++ List.filter (fun x ↦ !decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList

Tactic:
exact filter_append_perm (· ∈ s) (primeFactorsList m)

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
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
replace h := h.1

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
let S : Set ℂ := {z | y < z.re}

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
by
  have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
  have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
  have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
    prod_mulIndicator_eq_prod_filter
      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
  have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
  simpa only [← H, H'] using this

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑n ^ 2 * T + -(S * 2 * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im

Tactic:
mul_comm S

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑n ^ 2 * T + -(2 * S * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
mul_comm _ ‖cexp _‖,

Goal state after:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (3 * π * ↑|n| ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 * ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) * (↑π * I * ↑n ^ 2)‖

Tactic:
mul_comm _ ‖cexp _‖,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (π * ↑|n| ^ 2) ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) * (↑π * I * ↑n ^ 2)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
obtain ⟨S, hz⟩ := exists_gt |im z|

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
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|))
⊢ ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n

Tactic:
refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_

Goal state after:
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|))
n : ℤ
p : ℂ × ℂ
hp : p ∈ V
⊢ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n p.1 p.2‖ ≤ u n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

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

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
⊢ ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨S, hz⟩ := exists_gt |im z|

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
⊢ ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (z, τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ) (2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * -(starRingEnd ℂ) z + ↑π * I * ↑n ^ 2 * -(starRingEnd ℂ) τ)

Tactic:
map_mul,

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ -((starRingEnd ℂ) 2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑n *
        (starRingEnd ℂ) (cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ))) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * -(starRingEnd ℂ) z + ↑π * I * ↑n ^ 2 * -(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ -((starRingEnd ℂ) 2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑n *
        cexp ((starRingEnd ℂ) (2 * ↑π * I * ↑n * z) + (starRingEnd ℂ) (↑π * I * ↑n ^ 2 * τ))) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * -(starRingEnd ℂ) z + ↑π * I * ↑n ^ 2 * -(starRingEnd ℂ) τ)

Tactic:
map_mul,

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ -((starRingEnd ℂ) 2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑n *
        cexp
          ((starRingEnd ℂ) 2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑n * (starRingEnd ℂ) z +
            (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) (↑n ^ 2) * (starRingEnd ℂ) τ)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * -(starRingEnd ℂ) z + ↑π * I * ↑n ^ 2 * -(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ sinKernel (-a) x = -sinKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
      neg_div]

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

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

Tactic:
congrm ?_ * cexp (?_ + ?_)

Goal state after:
case refine_1
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) = 2 * ↑π * I * ↑n

case refine_2
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * I * ↑n * ↑a

case refine_3
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -↑π * ↑n ^ 2 * ↑t = ↑π * I * ↑n ^ 2 * (I * ↑t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) (sinKernel (↑a) t)

Tactic:
rw [← hasSum_ofReal]

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * ↑x * Real.sin (2 * π * a * ↑x) * rexp (-π * ↑x ^ 2 * t))) ↑(sinKernel (↑a) t)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun n_1 ↦ χ ↑n_1) ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ

Tactic:
nth_rewrite 1 [← mul_one ↗χ]

Goal state after:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun n_1 ↦ χ ↑n_1) * 1 ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case neg
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
n : ℕ
h : ¬n = 0
⊢ s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s =
    s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2

Tactic:
simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_natCast, Complex.cos,
      show 2 * π * a * n * I = 2 * π * I * a * n by ring, neg_mul, mul_div_assoc,
      div_right_comm _ (2 : ℂ), Int.cast_natCast, Nat.abs_cast, Int.cast_neg, mul_neg, abs_neg, ←
      mul_add, ← add_div]

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

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

Tactic:
exact LSeries_congr (fun _ ↦ by simp [mul_comm, logMul]) s

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

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ 0 < (a ^ 2) ^ 2 + (b ^ 2) ^ 2

Tactic:
exact
    add_pos (sq_pos_of_ne_zero (pow_ne_zero 2 h.1)) (sq_pos_of_ne_zero (pow_ne_zero 2 h.2.1))

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

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
⊢ False

Tactic:
have htt : PythagoreanTriple a n m := by
    delta PythagoreanTriple
    linear_combination ht1

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ h.IsClassified

Tactic:
convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc) <;>
    rw [Int.mul_ediv_cancel']

Goal state after:
case e'_1
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ x

case e'_2
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ y

case e'_3
x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ ↑(x.gcd y) ∣ z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
⊢ (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)).1 ^ 2 + (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)).2 ^ 2 = 1

Tactic:
by field [hk x]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ a.wronskian a = 0

Tactic:
wronskian,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ a * derivative a - derivative a * a = 0
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a.wronskian b = 0
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
wronskian,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b - derivative a * b = 0
⊢ derivative a = 0 ∧ derivative b = 0
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ c.natDegree + 1 ≤ abc_r.natDegree

Tactic:
apply Nat.lt_of_add_lt_add_left

Goal state after:
case a
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := ⋯
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := ⋯
⊢ ?n + c.natDegree < ?n + abc_r.natDegree

case n
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := ⋯
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := ⋯
⊢ ℕ
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
h : IsCoprime (radical a * EuclideanDomain.divRadical a) b
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
rw [← radical_mul_divRadical (a := b)] at h

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: case refine_1.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ (algebraMap (𝓞 K) K) (↑(Ideal.absNorm (↑I).num) * a) = ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a

Tactic:
map_mul,

Goal state after:
case refine_1.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ (algebraMap (𝓞 K) K) ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a =
    ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a