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

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k 0 + 0 = 2 ^ k / 2 * (0 + bernoulliFun k (1 / 2 + 0 / 2) + (bernoulliFun k 0 + 0))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
bernoulliFun_eval_zero,

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : ↑(bernoulli k) + 0 = 2 ^ k / 2 * (0 + bernoulliFun k (1 / 2 + 0 / 2) + (↑(bernoulli k) + 0))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ ∑ j ∈ {0}, Φ j * completedHurwitzZetaEven (toAddCircle j) s = Φ 1 * completedRiemannZeta s

Tactic:
sum_singleton,

Goal state after:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 0 * completedHurwitzZetaEven (toAddCircle 0) s = Φ 1 * completedRiemannZeta s
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: 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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)}) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
span_union,

Goal state after:
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span {(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)}) =
    span ↑(Ideal.map (algebraMap R S) I) ⊔ span {(aeval x) Q}
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * (↑n + 1) ^ ↑x / ↑m ^ ↑x = z / (↑m / (↑n + 1)) ^ ↑x

Tactic:
div_eq_mul_inv z,

Goal state after:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * (↑n + 1) ^ ↑x / ↑m ^ ↑x = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
⊢ DifferentiableAt ℂ B.F s

Tactic:
by
  apply DifferentiableAt.congr_of_eventuallyEq
  · exact (differentiableAt_riemannZeta hs).mul <| differentiableAt_LFunction B.χ s (.inl hs)
  · filter_upwards [eventually_ne_nhds hs] with t ht using Function.update_of_ne ht ..

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ ∑' (b : ℕ), (3 * (↑a ^ b / ↑b).re + 4 * ((↑a * z) ^ b / ↑b).re + ((↑a * z ^ 2) ^ b / ↑b).re)

Tactic:
refine tsum_nonneg fun n ↦ ?_

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re
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
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hG : AnalyticOnNhd ℂ G U := by
    refine DifferentiableOn.analyticOnNhd
      (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo
    apply ((differentiableAt_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul
    apply differentiableAt_completedLFunction _ _ (ht.1.imp_right fun h ↦ dft_apply_zero Φ ▸ h)
    exact ht.2.imp_right (fun h ↦ by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero])

Goal state after:
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
hUp : IsPreconnected U
hF : AnalyticOnNhd ℂ F U
hG : AnalyticOnNhd ℂ G U
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
⊢ Summable F''

Tactic:
have hp₁ (p : Nat.Primes) : (p : ℝ)⁻¹ < 1 :=
    (inv_lt_one₀ <| mod_cast p.prop.pos).mpr <| Nat.one_lt_cast.mpr <| p.prop.one_lt

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable F''
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
⊢ Summable (F₀ ∘ Subtype.val)

Tactic:
have hFF' :
      F₀ ∘ Subtype.val (p := fun n ↦ n ∈ {n | IsPrimePow n}) = F' ∘ ⇑prodNatEquiv.symm := by
    refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_
    ext1 n
    simp only [Function.comp_apply, F']
    congr

Goal state after:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F₀ ∘ Subtype.val)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x ↦ LSeries f ↑x) x = 0 x

Tactic:
by simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ Tendsto (fun n ↦ ∑ i ∈ range (n + 1), LSeries.term f s i) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))

Tactic:
Nat.range_succ_eq_Icc_zero,

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ Tendsto (fun n ↦ ∑ x ∈ Icc 0 n, LSeries.term f s x) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
rw [← LSeries_congr fun _ ↦ if_neg _, LSeries_eq_mul_integral_aux (if_pos rfl) hr hs hS]

Goal state after:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, if k = 0 then 0 else f k) * ↑t ^ (-(s + 1)) =
    s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) =O[atTop] fun n ↦ ↑n ^ r

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ ∀ {n : ℕ}, n ≠ 0 → ¬n = 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : Nat.Prime a_1 ∧ a_1 ∣ b), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ p ∣ b

Tactic:
exists_prop,

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, (Nat.Prime a_1 ∧ a_1 ∣ b) ∧ ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ p ∣ b
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯ =
    List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯

Tactic:
apply List.pmap_congr_left

Goal state after:
a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ ∀ a_1 ∈ b.primeFactorsList, ∀ (h₁ : Nat.Prime a_1), Nat.Prime a_1 → legendreSym a_1 a = (⇑χ ∘ Nat.cast) a_1
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
⊢ ∀ ε > 0, ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε

Tactic:
intro ε εpos

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
⊢ (if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
    else
      if ha1 : a = 1 then if flip = true then -1 else 1
      else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
split <;> rename_i ha2

Goal state after:
case ind.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

case ind.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
⊢ (if ha1 : a = 1 then if flip = true then -1 else 1
    else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * (x * y)) = y * a

Tactic:
by rw [hy, mul_one]

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

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x, ∃ (_ : x ∈ IsLocalRing.maximalIdeal ↥v.integer), ¬x = 0

Tactic:
exists_prop,

Goal state after:
K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x ∈ IsLocalRing.maximalIdeal ↥v.integer, ¬x = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑(sMod p (p - 2)) = 0

Tactic:
rw [h]

Goal state after:
case mpr
p : ℕ
w : 1 < p
h : sMod p (p - 2) = 0
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:

Tactic:
n = #𝒜 := ?_
    _ ≤ #(𝒜 \\ 𝒜) := 𝒜.card_le_card_diffs
    _ ≤ #(Ioo 0 n) := card_le_card_of_injOn (fun s ↦ ∏ p ∈ s, p) ?_ ?_
    _ = n - 1 := by rw [card_Ioo, tsub_zero]
    _ < n := tsub_lt_self hn.bot_lt zero_lt_one

Goal state after:
case calc_1
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ n = #𝒜

case calc_2
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.MapsTo (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜) ↑(Ioo 0 n)

case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.InjOn (fun s ↦ ∏ p ∈ s, p) ↑(𝒜 \\ 𝒜)
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
h : f a / (f a).gcd (f b) = f c / (f c).gcd (f d)
⊢ (f a / (f a).gcd (f b)).primeFactors = (f c / (f c).gcd (f d)).primeFactors

Tactic:
rw [h]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 3 = (ZMod.castHom ⋯ (X q)) 3

Tactic:
map_ofNat

Goal state after:
k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
q : ℕ := 2 * k + 1
this : 3 ^ k = -1
⊢ 3 = 3
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
⊢ ∃ n, 0 < n ∧ IsPrimitiveRoot z n

Tactic:
by
  obtain ⟨_, _, hz_pow⟩ := pow_eq_one_of_mahlerMeasure_eq_one h hz₀ hz
  exact IsPrimitiveRoot.exists_pos hz_pow (by omega)

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 ^ ((q + 1) / 2) * ω ^ ((q + 1) / 2) = -2
⊢ 2 = (ZMod.castHom ⋯ (X q)) 2

Tactic:
map_ofNat

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 ^ ((q + 1) / 2) * ω ^ ((q + 1) / 2) = -2
⊢ 2 = 2
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst✝ : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
⊢ DiscreteTopology ↥(H.subgroupOf K) ↔ DiscreteTopology ↥K

Tactic:
discreteTopology_iff_of_finiteIndex

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst✝ : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
⊢ DiscreteTopology ↥K ↔ DiscreteTopology ↥K
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

Tactic:
intro o
    have ω_pow :=
      congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) <|
        orderOf_dvd_iff_pow_eq_one.1 o
    have h : (1 : ZMod (q (p' + 2))) = -1 :=
      congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
    have : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
    apply ZMod.neg_one_ne_one h.symm

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
clear_value p'

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

Goal state before:
pp: p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ := p - 2
hp' : p' = p - 2
⊢ LucasLehmerTest p

Tactic:
clear_value p'

Goal state after:
p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
⊢ LucasLehmerTest p
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ a * b ∈ {g | ↑(↑g 1 0) = 0}

Tactic:
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
    simp only [coe_mul, Set.mem_ofPred_eq] at *
    simp [h, ha, hb]

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

Goal state before:
pp: case mp
N : ℕ
A : ↥(Gamma0 N)
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul, ha, Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero,
      sub_zero] using adet

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

Goal state before:
pp: case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ.relIndex (Γ ⊓ Γ') ≠ 0

Tactic:
rw [relIndex_eq_one.mpr inf_le_left]

Goal state after:
case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : j ∈ toConjAct g⁻¹ • Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
map_inv,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : j ∈ (toConjAct g)⁻¹ • Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.strictWidthInfty ↔ IsCusp ∞ 𝒢

Tactic:
by
  constructor
  · refine fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩
    · rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]
      simpa using h.ne'
    · simp [smul_infty_eq_self_iff]
  · -- Hard implication: if `∞` is a cusp, show the strict width is positive.
    rintro ⟨g, hgg, hgp, hgi⟩
    apply 𝒢.strictWidthInfty_nonneg.lt_of_ne'
    rw [← AddSubgroup.zmultiples_ne_bot]
    simp only [AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, AddSubgroup.mk_eq_zero,
      exists_prop, and_comm, ← strictPeriods_eq_zmultiples_strictWidthInfty, mem_strictPeriods_iff]
    -- We have some `g ∈ 𝒢` which is parabolic and fixes `∞`. So `g = ±[1, x; 0, 1]` some `x ≠ 0`.
    rw [smul_infty_eq_self_iff] at hgi
    rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp
    rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩
    · -- If `g = [1, x; 0, 1]`, we're done
      exact ⟨x, hx, hgg⟩
    · -- If `g = -[1, x; 0, 1]` then `g ^ 2 = [1, 2 * x; 0, 1]`.
      exact ⟨2 • x, by grind,
        by simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2⟩

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

Goal state before:
pp: N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
a : ℤ
ha : (Int.castAddHom ℝ) (a • ↑N) = x
⊢ ↑(↑(ModularGroup.T ^ (a * ↑N)) 0 0) = 1 ∧
    ↑(↑(ModularGroup.T ^ (a * ↑N)) 0 1) = 0 ∧
      ↑(↑(ModularGroup.T ^ (a * ↑N)) 1 0) = 0 ∧ ↑(↑(ModularGroup.T ^ (a * ↑N)) 1 1) = 1

Tactic:
by simp [ModularGroup.coe_T_zpow]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = (-1) ^ k * f z
⊢ f z = 0 z

Tactic:
hk.neg_one_zpow

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

Tactic:
rw [qExpansionFormalMultilinearSeries,
    ← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map]
  simp

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
let R := Real.exp (-2 * π * t / h)

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
⊢ Pairwise (Disjoint on gammaSet N r)

Tactic:
by
  refine fun u v huv ↦ ?_
  contrapose huv
  obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv
  exact hf.1.1.symm.trans hf.2.1

Goal state after: