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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
x✝¹ : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
b : 𝓞 K
x✝ : b ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
h : ↑a / ↑n = ↑b / ↑n
⊢ a = b

Tactic:
div_left_inj' hn',

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
x✝¹ : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
b : 𝓞 K
x✝ : b ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
h : ↑a = ↑b
⊢ a = b
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case hl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
⊢ ({ toFun := fun x ↦ h.repr x %ₘ f, map_add' := ⋯ } x).coeff i = 0

Tactic:
obtain rfl | hf := eq_or_ne f 1

Goal state after:
case hl.inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial R
i : ℕ
h : IsAdjoinRootMonic S 1
hi : natDegree 1 ≤ i
⊢ ({ toFun := fun x ↦ h.repr x %ₘ 1, map_add' := ⋯ } x).coeff i = 0

case hl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hf : f ≠ 1
⊢ ({ toFun := fun x ↦ h.repr x %ₘ f, map_add' := ⋯ } x).coeff i = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
⊢ (h.lift (algebraMap R S) h.root ⋯) x = x

Tactic:
by
  rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_root_eq_map]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ J ∉
    Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

Tactic:
Multiset.mem_map

Goal state after:
case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ ¬∃ a ∈ (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach,
      ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm a) = J
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
⊢ bernoulliFun k (↑m * x) = ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)

Tactic:
suffices h : ∀ x, f k x = 0 by
    rw [← sub_eq_zero]
    exact h x

Goal state after:
k m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
⊢ ∀ (x : ℝ), f k x = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case zero
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
⊢ ∀ (x : ℝ), f 0 x = 0

Tactic:
| zero =>

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
rw [LSeries, ← tsum_mul_left, (hs hx).tsum_eq_add_tsum_ite (n + 1), pow_mul_term_eq f x n]

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ (f (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) n_1) = f (n + 1) + ∑' (m : ℕ), F x m
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
⊢ Uc.Countable

Tactic:
apply Countable.union <;>
      split_ifs

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
h✝ : ∑ j, Φ j = 0
⊢ ∅.Countable

case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
h✝ : ¬∑ j, Φ j = 0
⊢ {0}.Countable

case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
h✝ : Φ 0 = 0
⊢ ∅.Countable

case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
h✝ : ¬Φ 0 = 0
⊢ {1}.Countable
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| -(2 * ↑π * I) ^ (2 * k + 1)

Tactic:
rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, pow_mul, I_sq]

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

Goal state before:
pp: case neg.refine_1.ind.zero
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
H' : ∀ (n : ℕ), (fun x ↦ ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x ↦ 0
ih : ∀ m < 0, F m = 0
⊢ Tendsto (fun x ↦ ↑0 ^ ↑x * LSeries F ↑x) atTop (nhds (F 0))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f 0 = g 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

Tactic:
have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by simp
    rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
      Polynomial.bernoulli_three_eval_one_quarter]
    simp [Nat.factorial]; ring

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 1 / 4 ∈ Icc 0 1

Tactic:
rw [mem_Icc]

Goal state after:
⊢ 0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(∑ x ∈ Ico 1 (p / 2).succ, (a * x % p + p * (a * x / p))) =
    ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑(a * x)).val) + ↑(∑ x ∈ Ico 1 (p / 2).succ, a * x / p)

Tactic:
simp only [val_natCast]
      simp [sum_add_distrib, ← mul_sum, Nat.cast_add, Nat.cast_mul, Nat.cast_sum, hp2]

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
t : ℝ
ht : t ∈ Set.Ici 1
⊢ ContinuousWithinAt (fun t ↦ ↑t ^ (-↑s - 1)) (Set.Ici 1) t

Tactic:
exact (continuousAt_ofReal_cpow_const _ _ <|
      Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
exact H.left

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

Goal state before:
pp: case refine_1
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ioi T) volume

pp: case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ε * t ^ (-s)) (Set.Ioi T) volume

pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
· exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁

Goal state after:
case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun t ↦ ε * t ^ (-s)) (Set.Ioi T) volume

case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case zero
a : ℤ
b : ℕ
⊢ J(a | b ^ 0) = J(a | b) ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b e : ℕ
⊢ J(a | b ^ e) = J(a | b) ^ e

Tactic:
induction e with

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ 0 ≤ ‖S t - l * ↑t‖ * t ^ (-1 - 1)

Tactic:
exact mul_nonneg (norm_nonneg _) <| Real.rpow_nonneg (zero_le_one.trans ht.1.le) _

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ qrSign (↑p) a * J(↑↑p | a) = J(↑a | p)

Tactic:
Nat.cast_id,

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ qrSign p a * J(↑p | a) = J(↑a | p)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = qrSign (↑q) p * J(↑↑q | p)

Tactic:
Nat.cast_id,

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = qrSign q p * J(↑q | p)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ J(↑a | b) = -J(↑b | a)

Tactic:
quadratic_reciprocity,

Goal state after:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ (-1) ^ (a / 2 * (b / 2)) * J(↑b | a) = -J(↑b | a)

case ha
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd a

case hb
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ Odd b
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case zero
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
⊢ i ≤ 1 → ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i

Tactic:
hi1

Goal state after:
case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
hj : c ∈ ⋃ i ∈ t, U i
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i

Tactic:
simp only [Set.mem_iUnion, exists_prop, U] at hj

Goal state after:
case inr.refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : (MonoidWithZeroHom.ofClass v) c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
hj : ∃ i ∈ t, c ∈ if v i ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v i}
⊢ ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a

Tactic:
legendreSym.to_jacobiSym,

Goal state after:
p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ J(a | p) = fastLegendreSym p a
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
⊢ 2 ^ k - 1 + 1 = 2 ^ k

Tactic:
tsub_add_cancel_of_le

Goal state after:
k : ℕ
⊢ 2 ^ k = 2 ^ k

k : ℕ
⊢ 1 ≤ 2 ^ k
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p' : ℕ
⊢ sZMod (p' + 2) 0 = ↑(s 0)

Tactic:
| zero =>

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)

Tactic:
refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_

Goal state after:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ 0 ≤ liminf (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)

case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

case refine_3
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q : ℕ
⊢ ↑(s 0) = ω ^ 2 ^ 0 + ωb ^ 2 ^ 0

Tactic:
dsimp [s, ω, ωb]
    ext <;> norm_num

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q : ℕ
⊢ ↑(s 0) = ω ^ 2 ^ 0 + ωb ^ 2 ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w✝ : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
⊢ ¬Nat.Prime (mersenne (p' + 2)) → ¬LucasLehmerTest (p' + 2)

Tactic:
intro a

Goal state after:
p' : ℕ
w✝ : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
a : ¬Nat.Prime (mersenne (p' + 2))
⊢ ¬LucasLehmerTest (p' + 2)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
hp : 2 ≤ p
⊢ ↑(sModNat (2 ^ p - 1) 0) = sMod p 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q : ℕ
⊢ sModNatAux (4 % q) q 0 = sModNat q 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
q✝ i q b : ℕ
⊢ sModNatTR.go q 0 b = sModNatAux b q 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ.zero
q✝ i q b : ℕ
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q 0 = (sModNatAux b q 0 ^ 2 + (q - 2)) % q

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬LucasLehmerTest p

Tactic:
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat]

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
this : Dense ↑⊤ ∨ ∃ a, zpowers a = ⊤
hA : DiscreteTopology ↥⊤
h : Dense ↑⊤
⊢ DiscreteTopology G

Tactic:
← (Homeomorph.Set.univ G).discreteTopology_iff

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
a✝ : Nontrivial G
this : Dense ↑⊤ ∨ ∃ a, zpowers a = ⊤
hA : DiscreteTopology ↥⊤
h : Dense ↑⊤
⊢ DiscreteTopology ↑Set.univ
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
⊢ g ^ 0 • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
⊢ f ∣[k] γ = fun τ ↦
    f (γ • τ) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

Tactic:
simp [SL_slash, slash_def, σ]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
τ : ℍ
⊢ (f ∣[k] γ) τ =
    f (γ • τ) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

Tactic:
simp [SL_slash, slash_def, σ]

Goal state after: