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

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

Tactic:
refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)
    · dsimp only at h
      exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro x (by simp [add_comm, *])))
    · apply Nat.le_add_left

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

Goal state before:
pp: case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
have : Nonneg ⟨_, _⟩ :=
      nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))

Goal state after:
case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
this : { re := -↑(x + z), im := ↑(y + w) }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
re_x im_x : ℤ
⊢ f { re := re_x, im := im_x } = g { re := re_x, im := im_x }

Tactic:
simp [decompose, h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ ↑(a * b).re + ↑(a * b).im * ↑r = (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r)

Tactic:
have :
          (a.re + a.im * r : R) * (b.re + b.im * r) =
            a.re * b.re + (a.re * b.im + a.im * b.re) * r + a.im * b.im * (r * r) := by
          ring
        simp only [re_mul, Int.cast_add, Int.cast_mul, im_mul, this, r.prop]
        ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : i = 0
j2 : j = 2
⊢ False

Tactic:
j2

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn✝ : j > n
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : i = 0
j2 : j = 2
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < 1 / ↑q.den ^ 2 ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Tactic:
(by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))

Goal state after:
ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : p ∈ k.primeFactorsList
⊢ k ≠ 0

Tactic:
by assumption

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ m ≠ 0

Tactic:
by assumption

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

Tactic:
exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1

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

Tactic:
enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]

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 (p ^ x.1) * f ↑x.2
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n k : ℕ
h✝ : ¬k = 0
⊢ k ≠ 0

Tactic:
by assumption

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

Goal state before:
pp: ⊢ (fun t ↦ (1 - rexp (-π * t))⁻¹) =O[atTop] fun x ↦ 1

Tactic:
refine ((Tendsto.const_sub _ ?_).inv₀ (by simp)).isBigO_one ℝ (c := ((1 - 0)⁻¹ : ℝ))

Goal state after:
⊢ Tendsto (fun x ↦ rexp (-π * x)) atTop (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: ⊢ Tendsto (fun x ↦ rexp (-π * x)) atTop (𝓝 0)

Tactic:
simpa only [neg_mul, tendsto_exp_comp_nhds_zero, tendsto_neg_atBot_iff]
    using! tendsto_id.const_mul_atTop pi_pos

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

Goal state before:
pp: case a
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -π * ((↑n + a) ^ 2 * t) ≤ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t)

Tactic:
rw [← sub_nonneg]

Goal state after:
case a
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r : ℝ
⊢ (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) =O[𝓝[>] 0] fun x ↦ x ^ r

Tactic:
by
  have := (P.hg_top (-(r + P.k))).comp_tendsto tendsto_inv_nhdsGT_zero
  simp_rw [IsBigO, IsBigOWith, eventually_nhdsWithin_iff] at this ⊢
  obtain ⟨C, hC⟩ := this
  use ‖P.ε‖ * C
  filter_upwards [hC] with x hC' (hx : 0 < x)
  have h_nv2 : ↑(x ^ P.k) ≠ (0 : ℂ) := ofReal_ne_zero.mpr (rpow_pos_of_pos hx _).ne'
  have h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0 := mul_ne_zero P.symm.hε h_nv2
  specialize hC' hx
  simp_rw [Function.comp_apply, ← one_div, P.h_feq' _ hx] at hC'
  rw [← ((mul_inv_cancel₀ h_nv).symm ▸ one_smul ℂ P.g₀ :), mul_smul _ _ P.g₀, ← smul_sub, norm_smul,
    ← le_div_iff₀' (lt_of_le_of_ne (norm_nonneg _) (norm_ne_zero_iff.mpr h_nv).symm)] at hC'
  convert! hC' using 1
  · congr 3
    rw [rpow_neg hx.le]
    simp [field]
  · simp_rw [norm_mul, norm_real, one_div, inv_rpow hx.le, rpow_neg hx.le, inv_inv, norm_inv,
      norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_add hx]
    field

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

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

Tactic:
rcases lt_trichotomy 1 x with hx' | rfl | hx'

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

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

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.LSeries.MellinEqDirichlet

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this✝ : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
this : 0 ≤ p i
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
norm_of_nonneg (by positivity)

Goal state after:
case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this✝ : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
this : 0 ≤ p i
⊢ ‖a i‖ / p i ^ s.re ≤ ‖a i‖ / p i ^ s.re
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

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
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1

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

Goal state after:
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
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
⊢ HasSum (fun i ↦ s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))

Tactic:
by
  have hs' : 0 < (s / 2).re := by rw [div_ofNat_re]; positivity
  simp_rw [← sq_eq_zero_iff (a := r _)] at hF
  convert! hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i
  · rw [← neg_div, Gammaℝ_def]
  · rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
    · ring_nf
    all_goals rw [arg_ofReal_of_nonneg (abs_nonneg _)]; linarith [pi_pos]
  · convert! h_sum using 3 with i
    rw [← sq_abs, ← rpow_natCast_mul (abs_nonneg _), div_ofNat_re, Nat.cast_ofNat,
      mul_div_cancel₀ _ two_pos.ne']

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

Goal state before:
pp: z τ : ℂ
| ∑' (x : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term x z τ

Tactic:
← (Equiv.addRight 1).tsum_eq

Goal state after:
z τ : ℂ
| ∑' (c : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term ((Equiv.addRight 1) c) z τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Tactic:
have (s : _) : completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) - (if b = 0 then 1 else 0)) / s := by
    simp_rw [completedHurwitzZetaEven_eq, sub_div]
    abel
  rw [funext this]
  refine .sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero
  apply DifferentiableAt.sub <;> apply differentiable_completedHurwitzZetaEven₀

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

Goal state before:
pp: case pos
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : n = 0
⊢ 0 ≤ 0

pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ¬↑n = 1
h✝ : ¬n = 0
⊢ 0 ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
all_goals positivity

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
refine tsum_congr fun n ↦ ?_

Goal state after:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ Summable fun n ↦ ‖(riemannZetaSummandHom ⋯) n‖

Tactic:
simp only [riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ Summable fun n ↦ ‖↑n ^ (-s)‖
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n ↦ ‖(dirichletSummandHom χ ⋯) n‖

Tactic:
by
  simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]
  exact (summable_riemannZetaSummand hs).of_nonneg_of_le (fun _ ↦ by positivity)
    (fun n ↦ mul_le_of_le_one_left (norm_nonneg _) <| χ.norm_le_one n)

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2)
    ((hurwitzOddFEPair ↑a).Λ ((s + 1) / 2) / 2)

Tactic:
(isStrong_hurwitzOddFEPair _).Λ_eq

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2)
    (mellin (hurwitzOddFEPair ↑a).f ((s + 1) / 2) / 2)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : Fin 4
⊢ z * z ≠ 2

Tactic:
fin_cases z

Goal state after:
case «0»
⊢ (fun i ↦ i) ⟨0, ⋯⟩ * (fun i ↦ i) ⟨0, ⋯⟩ ≠ 2

case «1»
⊢ (fun i ↦ i) ⟨1, ⋯⟩ * (fun i ↦ i) ⟨1, ⋯⟩ ≠ 2

case «2»
⊢ (fun i ↦ i) ⟨2, ⋯⟩ * (fun i ↦ i) ⟨2, ⋯⟩ ≠ 2

case «3»
⊢ (fun i ↦ i) ⟨3, ⋯⟩ * (fun i ↦ i) ⟨3, ⋯⟩ ≠ 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
⊢ False

Tactic:
have hf : Fermat42 a1 b1 c1 :=
    (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1

Goal state after:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
inv_Gammaℝ_two_sub hs,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s

Tactic:
inv_Gammaℝ_two_sub hs,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree + b.degree < a.degree + b.degree

Tactic:
WithBot.add_lt_add_iff_right hb

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b.degree ≠ ⊥
⊢ (derivative a).degree < a.degree
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ y = m ^ 2 - n ^ 2 ∧ z = m ^ 2 + n ^ 2

Tactic:
apply Rat.div_int_inj hzpos hm2n2 (h.coprime_of_coprime hc) H

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ ↑y / ↑z = ↑(m ^ 2 - n ^ 2) / ↑(m ^ 2 + n ^ 2)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
obtain rfl | ha := eq_or_ne a 0
  · simp
  obtain rfl | hb := eq_or_ne b 0
  · simp
  nontriviality M
  simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
suffices range (ofReal : ℝ → ℂ) ⊆ K by
    rw [range_subset_iff, ← coe_algebraMap] at this
    have :=
      (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
        (Subfield.toIntermediateField K this).toSubalgebra
    simp_rw [← SetLike.coe_set_eq, IntermediateField.coe_toSubalgebra] at this ⊢
    exact this

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ↑K
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 : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥

Tactic:
exact LinearMap.ker_eq_bot.mpr (IsFractionRing.injective R K)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ { φ // ComplexEmbedding.IsReal φ } ≃ { w // w.IsReal }

Tactic:
by
  refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
  · exact ⟨φ, φ.prop, rfl⟩
  · rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self,
      ← Subtype.ext_iff] at h
  · exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ‖∏ σ, σ x‖

Tactic:
rw [norm_prod, ← Fintype.prod_equiv (RingHom.equivRatAlgHom K ℂ) (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ∏ x_1, ‖x_1 x‖
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr.hi.hab
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ IsCoprime ca cb

Tactic:
apply (isCoprime_expand chn0).mp

Goal state after:
case inr.hi.hab
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ⋯
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ IsCoprime ((expand k ch) ca) ((expand k ch) cb)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
have main : w = InfinitePlace.mk ψ.toRingHom := by
      simp only [RingHom.toRatAlgHom_apply] at hψ
      rw [← norm_embedding_eq, hψ] at h
      contrapose! h
      exact h₂ h.symm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w = mk ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ℚ[↑x] = ⊤

Tactic:
rw [← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite ℚ _)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ℚ⟮↑x⟯.toSubalgebra = ⊤