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

Goal state before:
pp: α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
⊢ C f

Tactic:
obtain ⟨f, pf⟩ := f
  induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg

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

Goal state before:
pp: c d x y z w : ℕ
xz : z ≤ x
yw : y ≤ w
xy : SqLe x c y d
⊢ c * z * z ≤ c * x * x

Tactic:
by gcongr

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

Goal state before:
pp: c d x y z w : ℕ
xz : z ≤ x
yw : y ≤ w
xy : SqLe x c y d
⊢ d * y * y ≤ d * w * w

Tactic:
by gcongr

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

Goal state before:
pp: d x y z w : ℕ
⊢ (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy zw

Goal state after:
case refine_1
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy zw

Goal state after:
case refine_2
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 m ≤ yn a1 n

Tactic:
e

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 n ≤ yn a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy zw

Goal state after:
case refine_3
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
⊢ SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ xn a1 m ≤ xn a1 n

Tactic:
e

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ xn a1 n ≤ xn a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy zw

Goal state after:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
⊢ SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
e

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 0 ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 n

Tactic:
e

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n

Tactic:
zify at *

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 :
  ↑(d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j) = (↑(d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1) * ↑(xn a1 j)
⊢ ↑(d a1) * ↑(yn a1 n) * ↑(yn a1 n) + 1 = ↑(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
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
⊢ #(Ico 0 ↑n) < #D

Tactic:
card_Icc,

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
⊢ #(Ico 0 ↑n) < (↑n + 1 - 0).toNat
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
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
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - (ξ - 1) * ↑v) * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this

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
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
Module: Mathlib.NumberTheory.EulerProduct.ExpLog

Goal state before:
pp: α : Type u_1
f : α → ℂ
hsum : Summable f
hg : DifferentiableAt ℂ (fun z ↦ log (1 - z)) 0
⊢ (fun z ↦ log (1 - z)) =O[𝓝 0] id

Tactic:
simpa only [sub_zero, log_one] using! hg.isBigO_sub

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 m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
prod_insert 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) ((∑' (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 : ∀ {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}
| fun x ↦ f ↑((equivProdNatFactoredNumbers hpp hp) x)

Tactic:
x

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 : ∀ {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}
x : ℕ × ↑(factoredNumbers s)
| f ↑((equivProdNatFactoredNumbers hpp hp) x)
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 ξ - ↑u' / ↑v| * (↑v / ↑u' / fract ξ) < (↑v * (2 * ↑v - 1))⁻¹ * (↑v / ↑u' / fract ξ)

Tactic:
by gcongr

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

Tactic:
by gcongr

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun n ↦ π * T * ↑n) atTop atTop

Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)

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

Goal state before:
pp: k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ |↑(Int.ofNat n) + a| ^ k * rexp (-π * (↑(Int.ofNat n) + a) ^ 2 * t) = (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t)

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ |↑↑n + a| ^ k * rexp (-π * (↑↑n + a) ^ 2 * t) = (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ |↑n + (1 - a)| ^ k * rexp (-π * (-(↑n + (1 - a))) ^ 2 * t) = (↑n + (1 - a)) ^ k * rexp (-π * (↑n + (1 - a)) ^ 2 * t)

Tactic:
neg_sq,

Goal state after:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ |↑n + (1 - a)| ^ k * rexp (-π * (↑n + (1 - a)) ^ 2 * t) = (↑n + (1 - a)) ^ k * rexp (-π * (↑n + (1 - a)) ^ 2 * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 0

Tactic:
by
  apply tsum_eq_zero_of_not_summable
  rw [summable_jacobiTheta₂_term_iff]
  exact not_lt.mpr hτ

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

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

Tactic:
rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]

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

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

Tactic:
neg_sq,

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑(n + 1)) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * -↑(n + 1)) * ↑(rexp (-π * (-↑(n + 1)) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + 1 - (1 + 1))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)

Tactic:
neg_sq,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑(n + 1)) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * -↑(n + 1)) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + 1 - (1 + 1))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
⊢ ↑(sinKernel (↑a) x) = jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)

Tactic:
by
  simp [sinKernel, re_eq_add_conj, jacobiTheta₂'_conj, map_ofNat]

Goal state after:
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‖

Tactic:
x

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)
x : ℝ
| ‖evenKernel a x - if a = 0 then 1 else 0‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
neg_sq,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ ↑(2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) =
    -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
      -I * -↑↑n * cexp (2 * ↑π * I * ↑a * -↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ↑n + a = 0
⊢ 0 = ↑0 / 2

pp: case neg
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬↑n + a = 0
⊢ 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)) = ↑(rexp (-π * (↑n + a) ^ 2 * t)) / 2

Tactic:
· rw [ofReal_zero, zero_div]

Goal state after:
case neg
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬↑n + a = 0
⊢ 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)) = ↑(rexp (-π * (↑n + a) ^ 2 * t)) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
by
    apply this.congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
    rw [hurwitzZetaEven, Function.update_of_ne hx]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I * cexp (↑(2 * π * a * ↑n) * I) / 2‖ = 1 / 2

Tactic:
norm_div,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I * cexp (↑(2 * π * a * ↑n) * I)‖ / ‖2‖ = 1 / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / s.Gammaℝ

Tactic:
mul_div_assoc _ (cexp _),

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * (cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s) / 2 / s.Gammaℝ
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
⊢ a ∈ s

Tactic:
by simp [s]

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
⊢ b ∈ s

Tactic:
by simp [s]

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
⊢ c ∈ s

Tactic:
by simp [s]

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ Associated (d * {A, B, C}.gcd id) d

Tactic:
grw [← Finset.gcd_mul_left', gcd_eq_gcd_image]

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ Associated ((image (fun x ↦ d * id x) {A, B, C}).gcd id) d
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s

Tactic:
intro b hb

Goal state after:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:

Tactic:
_ = ∑' (p : Primes) (k : ℕ), (χ (p ^ (k + 1)) * ((p ^ (k + 1) : ℕ) : ℂ) ^ (-s)) *
          Λ (p ^ (k + 1)) / Real.log (p ^ (k + 1)) := by
      refine tsum_congr fun p ↦ tsum_congr fun k ↦ ?_
      have : Complex.log p ≠ 0 := mod_cast p.prop.log_ne_zero
      simp [mul_pow, ← cpow_nat_mul, ← natCast_cpow_natCast_mul, vonMangoldt_apply_pow,
        vonMangoldt_apply_prime p.2, field]
    _ = ∑' n : {n : ℕ // IsPrimePow n}, f n := by
      rw [← tsum_primes_pow_eq]
      · exact tsum_congr fun p ↦ tsum_congr fun k ↦ (by unfold f; simp; ring)
      · apply comp_injective _ Subtype.coe_injective (f := f)
        apply of_norm_bounded_eventually_nat (g := (↑· ^ (-s.re)))
        · simp [hs]
        · filter_upwards [eventually_gt_atTop 1] with n hn
          simp only [f, norm_mul, norm_div, norm_real, norm_eq_abs]
          grw [norm_le_one, vonMangoldt_le_log]
          have := log_pos (x := n) (mod_cast hn)
          field_simp
          rw [← ofReal_natCast n, norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)]
          simp
    _ = _ := by
      simp only [div_eq_mul_inv _ (_ ^ _), ← cpow_neg]
      suffices (Function.support f) ⊆ {n | IsPrimePow n} from
        tsum_subtype_eq_of_support_subset this
      intro n hn
      contrapose! hn
      simp [f, vonMangoldt_eq_zero_iff.mpr hn]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * m * n).natAbs = 1

Tactic:
(by ring : 2 * m * n = 2 * n * m),

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * n * m).natAbs = 1
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ -b.wronskian a

Tactic:
dvd_neg

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ b.wronskian a
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
this : Nontrivial M
p : M
⊢ p ∈ primeFactors (radical a) ↔ p ∈ primeFactors a

Tactic:
simp +contextual [mem_primeFactors, mem_normalizedFactors_iff',
    dvd_radical_iff_of_irreducible, ha₀]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + (-1) ^ 2 = 1
hw1 : w = -1
⊢ v = 0

Tactic:
neg_sq,

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + 1 ^ 2 = 1
hw1 : w = -1
⊢ v = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ (q * r + r * p + p * q) * (a + b + c) ≤ p * q * r * (a + b + c)

Tactic:
by gcongr

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ False

Tactic:
have h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2 := by
      apply Rat.div_int_inj hzpos _ (h.coprime_of_coprime hc) h1.2.2.2
      · change w = _
        rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]
        rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2, Rat.divInt_eq_div]
        norm_cast
      · lia

Goal state after:
case neg.inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2
⊢ False