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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
⊢ Fintype.card (Fin pb.dim) = Fintype.card (L →ₐ[K] E)

Tactic:
rw [Fintype.card_fin, AlgHom.card]

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
⊢ pb.dim = n
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) =
    ∏ σ, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
prod_prod_Ioi_mul_eq_prod_prod_off_diag

Goal state after:
case e_a
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∏ i, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) = ∏ σ, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = re 0

Tactic:
apply eq_zero_of_mul_self_eq_zero

Goal state after:
case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im = im 0

Tactic:
apply eq_zero_of_mul_self_eq_zero

Goal state after:
case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
by
    let t := le_antisymm yx xy
    rw [one_mul] at t
    exact absurd t (not_divides_sq _ _)

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

Tactic:
have hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Goal state after:
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
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 * n
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
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ 2 * n - (j + 1) < 2 * n - j

Tactic:
rw [Nat.sub_succ]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
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
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ (2 * n - j).pred < 2 * n - j
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos

Goal state after:
ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
hq₀ : 0 < ↑q.den
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
h :
  ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom),
    (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}

Tactic:
show (x ::ₒ v) ∘ some = v from funext fun s => rfl

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
Module: Mathlib.NumberTheory.EulerProduct.ExpLog

Goal state before:
pp: f : ℕ →*₀ ℂ
hsum : Summable fun x ↦ ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
have H := hsum.of_norm.clog_one_sub.neg.subtype Nat.Prime |>.hasSum.cexp.tprod_eq

Goal state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x ↦ ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H :
  ∏' (b : Subtype Nat.Prime), (cexp ∘ (fun b ↦ -log (1 - f b)) ∘ Subtype.val) b =
    cexp (∑' (b : Subtype Nat.Prime), ((fun b ↦ -log (1 - f b)) ∘ Subtype.val) b)
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: case refine_1
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable f ↑x

pp: case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x

Tactic:
· exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ (le_max_left ..).trans_lt hx

Goal state after:
case refine_2
F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ
hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s
f g : ℕ → ℂ
x : ℝ
hx : max (abscissaOfAbsConv f) (abscissaOfAbsConv g) < ↑x
⊢ LSeriesSummable g ↑x
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < LSeries a ↑x

Tactic:
rw [LSeries]
  refine Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
  exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun x ↦ -((fun x ↦ -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x ↦ -1 * ↑x) x) atTop atTop

Tactic:
Pi.sub_apply

Goal state after:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun x ↦ -(-π * (T * ↑x ^ 2 - 2 * S * ↑x) - -1 * ↑x)) atTop atTop
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
← ofReal_pow,

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
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
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
have hp' i : a' i = 0 ∨ 0 < p i := by
    simp only [a']
    split_ifs with h <;> try tauto
    exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
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
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (P.f t + (Ioi 1).indicator (fun x ↦ P.f x) t) = ↑t ^ (s - 1) • P.f t

Tactic:
indicator_of_notMem (by grind),

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (P.f t + 0) = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (P.f t + (Ioo 0 1).indicator (fun x ↦ P.f x) t) = ↑t ^ (s - 1) • P.f t

Tactic:
indicator_of_notMem (by grind),

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (P.f t + 0) = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ riemannZeta 0 = -1 / 2

Tactic:
by
  simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

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

Goal state before:
pp: this : Tendsto (fun s ↦ ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Tactic:
apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_

Goal state after:
this : Tendsto (fun s ↦ ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
s : ℝ
⊢ ((fun s ↦ (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) ∘ fun s ↦ ↑s) s = ↑((s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine (h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)

Goal state after:
a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] (1 / 2)) (𝓝 1)
s : ℂ
⊢ ((fun s ↦ (s - 1 / 2) * (hurwitzEvenFEPair a).Λ s) ∘ fun s ↦ s / 2) s = (s - 1) * completedHurwitzZetaEven a s
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
this : 1 / 2 ≤ S
⊢ 1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
by
    convert! this using 5
    rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
    ring

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | k ≤ p}

Tactic:
by simpa [primesBelow, hpp] using hp₂

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ completedHurwitzZetaEven (↑a) s = mellin (fun t ↦ ↑(evenKernel (↑a) t) - if ↑a = 0 then 1 else 0) (s / 2) / 2

Tactic:
refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm

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

Goal state before:
pp: case inl
s : ℂ
hs : 1 < s.re
χ : DirichletCharacter ℂ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
· simp [modZero_eq_delta, delta_mul_eq_smul_delta, LSeries_delta]

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
    (hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ s * Λ s / s / s.Gammaℝ = Λ s / s.Gammaℝ

Tactic:
mul_div_cancel_left₀ _ hs

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ Λ s / s.Gammaℝ = Λ s / s.Gammaℝ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) 0

Tactic:
· -- Hard case : `s = 0`
    simp_rw [← claim2.limUnder_eq]
    have S_nhds : {(1 : ℂ)}ᶜ ∈ 𝓝 (0 : ℂ) := isOpen_compl_singleton.mem_nhds hs'
    refine ((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
      (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds
    simp only [Gammaℝ, zero_div, div_zero, Complex.Gamma_zero, mul_zero, sub_zero]
    -- Remains to show completed zeta is `o (s ^ (-1))` near 0.
    refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_
    rw [isLittleO_iff_tendsto']
    · exact Tendsto.congr (fun x ↦ by rw [← one_div, one_div_one_div]) nhdsWithin_le_nhds
    · exact eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim

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

Goal state before:
pp: n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
tfae_have 2 → 3
  | h, a, b, c, ha, hb, hc, habc => by
    rw [← Rat.num_ne_zero] at ha hb hc
    refine h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num)
      (by positivity) (by positivity) (by positivity) ?_
    have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
    refine Int.cast_injective <| (div_left_inj' this).1 ?_
    push_cast
    simp only [add_div, ← div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
      div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0),
      one_mul, mul_one, Rat.num_div_den, habc]

Goal state after:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
tfae_2_to_3 : FermatLastTheoremWith ℤ n → FermatLastTheoremWith ℚ n
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
by
  obtain ⟨l, m, n, ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co⟩⟩ := hc <;> use k * l, m, n <;> grind

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
simpa only [eq_neg_iff_add_eq_zero, one_pow] using hk 1

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

Goal state before:
pp: hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
⊢ FermatLastTheorem

Tactic:
intro n h
  obtain hdvd | ⟨p, hpprime, hdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt h
    <;> apply FermatLastTheoremWith.mono hdvd
  · exact fermatLastTheoremFour
  · exact hprimes p hpprime hpodd

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

Goal state before:
pp: case neg.refine_2
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
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ b.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
← mul_rotate

Goal state after:
case neg.refine_2
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
abc_dr_dvd_w : divRadical (c * a * b) ∣ w
hw : ¬w = 0
⊢ b.natDegree + 1 ≤ (radical (c * a * b)).natDegree
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : FractionalIdeal (𝓞 K)⁰ K
⊢ ↑I.den ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero I.den

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inl.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 : ℚ := ⋯
w : ℚ := ⋯
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 : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
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 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1

Tactic:
exact And.intro hm2 hn2

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
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 : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
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 = 0
⊢ m % 2 = 1 ∧ n % 2 = 0

Tactic:
exact And.intro hm2 hn2

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

Goal state before:
pp: case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
cases
      Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with
    | inl h =>
        left; ext1 x
        conv_rhs => rw [← hiφ x]
        exact (congrFun h (ι x)).symm
    | inr h =>
        right; ext1 x
        conv_rhs => rw [← hiφ x]
        exact (congrFun h (ι x)).symm

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ (mk φ).embedding = φ

Tactic:
by
  have := embedding_mk_eq φ
  rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this

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

Goal state before:
pp: case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| mk x✝ = mk w.embedding

pp: case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24

Tactic:
mk_eq_iff,

Goal state after:
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| x✝ = w.embedding ∨ ComplexEmbedding.conjugate x✝ = w.embedding

case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24