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

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

Tactic:
skip

Goal state after:
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k)
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
t : ℂ
ht : t ∈ U
h : Φ 0 = 0
⊢ ∑ j, 𝓕 Φ j = 0

Tactic:
by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero]

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

Goal state before:
pp: case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (↑↑p)⁻¹ ≤ 2⁻¹

Tactic:
inv_le_inv₀ (mod_cast p.prop.pos) zero_lt_two

Goal state after:
case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 2 ≤ ↑↑p
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ ContinuousAt (fun x ↦ ↑x + (1 + I * ↑y)) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
skip

Goal state after:
case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| (2 * ↑π) ^ (2 * k + 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine (continuousOn_neg_logDeriv_LFunctionTrivChar₁ q).mono fun s hs ↦ ?_
    simp only [ne_eq, Set.mem_ofPred_eq] at hs
    tauto

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n ↦ ↑(residueClass a n)) ↑x - (↑q.totient)⁻¹ / (↑x - 1) =
    ↑(L (fun n ↦ ↑(residueClass a n)) ↑x).re - ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Tactic:
congr 1

Goal state after:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n ↦ ↑(residueClass a n)) ↑x = ↑(L (fun n ↦ ↑(residueClass a n)) ↑x).re

case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Tactic:
obtain ⟨C, hC⟩ := bddBelow_def.mp <| IsCompact.bddBelow_image isCompact_Icc this

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ y ∈ (fun x ↦ (LFunctionResidueClassAux a ↑x).re) '' Set.Icc 1 2, C ≤ y
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
H : LSeries f = LSeries g
n : ℕ
hn : n ≠ 0
⊢ (fun x ↦ LSeries f ↑x) =ᶠ[Filter.atTop] fun x ↦ LSeries g ↑x

Tactic:
exact Filter.Eventually.of_forall fun x ↦ congr_fun H x

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)

Tactic:
skip

Goal state after:
case a
k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1)
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
Polynomial.bernoulli_three_eval_one_quarter

Goal state after:
this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ (-1) ^ (1 + 1) * (2 ^ 3 * π ^ 3) / 2 / ↑3! * (algebraMap ℚ ℝ) (3 / 64) = π ^ 3 / 32
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ IntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume

Tactic:
have h : LocallyIntegrableOn (fun t : ℝ ↦ ‖S t‖ * (t ^ (-s - 1))) (Set.Ici 1) := by
    refine hS₁.norm.mul_continuousOn ?_ isLocallyClosed_Ici
    exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt
  refine h.integrableOn_of_isBigO_atTop (g := fun t ↦ t ^ (-s)) (isBigO_iff.mpr ⟨ε, ?_⟩) ?_
  · filter_upwards [eventually_ge_atTop T, eventually_gt_atTop 0] with t ht ht'
    simpa [abs_of_nonneg, Real.rpow_nonneg, ht'.le, Real.rpow_sub ht', mul_assoc, ht'.ne',
      mul_div_cancel₀] using mul_le_mul_of_nonneg_right (hS₂ t ht) (norm_nonneg <| t ^ (-s - 1))
  · exact integrableAtFilter_rpow_atTop_iff.mpr <| neg_lt_neg_iff.mpr hs

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}) +
      #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    p / 2 * (q / 2)

Tactic:
hswap,

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hdisj :
  Disjoint ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})
    ({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
hunion :
  {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} ∪
      {x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p} =
    Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
⊢ #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q}) +
      #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p}) =
    p / 2 * (q / 2)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: 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
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * t ^ (-s - 1)

Tactic:
rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑↑a * ↑x).val}) % 2) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)

Tactic:
(by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ (#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}) % 2) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)
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)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
⊢ ContinuousOn (fun t ↦ l * ↑t) (Set.Ici 1)

Tactic:
by fun_prop

Goal state after:
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 ⋯).prod =
    (List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod

Tactic:
congr 1

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
⊢ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯ =
    List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
⊢ J(↑a | b) = qrSign b a * J(↑b | a)

Tactic:
by
  -- define the right-hand side for fixed `a` as a `ℕ →* ℤ`
  let rhs : ℕ → ℕ →* ℤ := fun a =>
    { toFun := fun x => qrSign x a * J(x | a)
      map_one' := by convert! ← mul_one (M := ℤ) _; (on_goal 1 => symm); all_goals apply one_left
      map_mul' := fun x y => by
        simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm] }
  have rhs_apply : ∀ a b : ℕ, rhs a b = qrSign b a * J(b | a) := fun a b => rfl
  refine value_at a (rhs a) (fun p pp hp => Eq.symm ?_) hb
  have hpo := pp.eq_two_or_odd'.resolve_left hp
  rw [@legendreSym.to_jacobiSym p ⟨pp⟩, rhs_apply, Nat.cast_id, qrSign.eq_iff_eq hpo ha,
    qrSign.symm hpo ha]
  refine value_at p (rhs p) (fun q pq hq => ?_) ha
  have hqo := pq.eq_two_or_odd'.resolve_left hq
  rw [rhs_apply, Nat.cast_id, ← @legendreSym.to_jacobiSym p ⟨pp⟩, qrSign.symm hqo hpo,
    qrSign.neg_one_pow hpo hqo, @legendreSym.quadratic_reciprocity' p q ⟨pp⟩ ⟨pq⟩ hp hq]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖↑↑u‖ = 1

Tactic:
simpa [← NNReal.coe_inj] using!
    (Valuation.integer.integers (NormedField.valuation (K := K))).valuation_unit u

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

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ χ₈ ↑b ^ e * (qrSign b a' * J(↑b | a')) = χ₈ ↑(b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))

Tactic:
congr 1

Goal state after:
case inr.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ χ₈ ↑b ^ e = χ₈ ↑(b % (4 * a)) ^ e

case inr.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' * J(↑b | a') = qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a')

Tactic:
congr 1

Goal state after:
case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ qrSign b a' = qrSign (b % (4 * a)) a'

case inr.e_a.e_a
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑b | a') = J(↑(b % (4 * a)) | a')
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : y < x
⊢ y < x

Tactic:
· simp [hxy]

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

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
⊢ (Set.Icc x y).Finite

Tactic:
· have H : (Set.Icc y⁻¹ 1).Finite := this _
      refine ((this x).union H.inv).subset (le_of_eq ?_)
      rw [Set.inv_Icc, inv_one, Set.Icc_union_Icc_eq_Icc] <;>
      simp [h, hy]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
x : K
hx : (valuation K) x ≤ (valuation K) r ^ 2
⊢ (valuation K) r ^ 2 < (valuation K) r

Tactic:
by simpa [pow_two, hr]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD 𝓂[K] ^ n • ⊤]

Tactic:
let S n : Set 𝒪[K] := f n +ᵥ ((𝓂[K] ^ n : Ideal 𝒪[K]) : Set 𝒪[K])
    have hS n : S (n + 1) ⊆ S n := by
      apply (Set.vadd_set_subset_vadd_set_iff.mpr (Ideal.pow_le_pow_right n.le_succ)).trans
      simpa [S] using (hf n.le_succ).symm
    have h n : IsClosed (S n) := (IsNoetherianRing.isClosed_ideal (𝓂[K] ^ n)).vadd (f n)
    obtain ⟨L, hL⟩ := (h 0).isCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed S hS
      (by simp [S]) h
    refine ⟨L, fun n ↦ ?_⟩
    obtain ⟨y, hy, rfl⟩ := Set.mem_iInter.mp hL n
    simpa [SModEq.sub_mem] using hy

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)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ =
    (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖S t - l * ↑t‖ * t ^ (-s - 1)

Tactic:
congr 1

Goal state after:
case e_a
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)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ = ∫ (t : ℝ) in Set.Ioi 1, ‖S t - l * ↑t‖ * t ^ (-s - 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: h : Prime (mersenne 1)
⊢ False

Tactic:
apply Nat.not_prime_one h

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
C ε : ℝ
⊢ ContinuousAt (fun s ↦ (s - 1) * s * C + s * ε) 1

Tactic:
by fun_prop

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‖
this : Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
⊢ ContinuousAt (fun s ↦ ↑s * l) 1

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:

Tactic:
‖z‖ ≤ max 1 ‖z‖ := le_max_right 1 ‖z‖
  _   ≤ ((p.map (castRingHom ℂ)).roots.map (fun a ↦ max 1 ‖a‖)).prod :=
        mem_le_prod_of_one_le (fun a ↦ le_max_left 1 ‖a‖) hz
  _   ≤ 1 := by grind [prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff,
        norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one]

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
have h_z_root : z ∈ p.aroots ℂ := by aesop

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ (X.ω ^ 2 ^ (p' + 2 - 2) + X.ωb ^ 2 ^ (p' + 2 - 2)).1 = 0

Tactic:
add_tsub_cancel_right

Goal state after:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ (A * B)) (f ((A * B) • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) * denom (A * B) ↑τ ^ (-k) =
    (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))

Tactic:
by
    rw [σ_mul_comm, σ_mul, denom_cocycle_σ, mul_zpow, mul_smul, map_mul, Units.val_mul,
      abs_mul, ofReal_mul, mul_zpow, map_zpow₀]

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)

Tactic:
refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩

Goal state after:
case refine_1
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p).IsParabolic

case refine_2
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p) • g • c = g • c
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case insert.inr
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ (|↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1)) •
      (f i ∣[k i] g * ∏ i ∈ t, f i ∣[k i] g) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ ↑(#t) • (f i ∣[k i] g * ∏ i ∈ t, f i ∣[k i] g)

Tactic:
congr 1

Goal state after:
case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ ↑(#t)
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } *
      denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^ (-k) =
    f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

Tactic:
simp [ModularGroup.S, denom]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
hH : DiscreteTopology ↑H
⊢ DiscreteTopology ↥𝒢.strictPeriods

Tactic:
have : Set.MapsTo upperRightHom 𝒢.strictPeriods H := fun x hx ↦ by
    grind [SetLike.mem_coe, Subgroup.mem_strictPeriods_iff]

Goal state after:
R : Type u_1
inst✝² : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
hG : DiscreteTopology ↥𝒢
H : Set (GL (Fin 2) R) := ↑𝒢 ∩ Set.range ⇑upperRightHom
hH : DiscreteTopology ↑H
this : Set.MapsTo (⇑upperRightHom) (↑𝒢.strictPeriods) H
⊢ DiscreteTopology ↥𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : x ∈ Subgroup.closure s
hf : f ∣[k] x = f
⊢ f ∣[k] x⁻¹ = f

Tactic:
← hf,

Goal state after:
case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : x ∈ Subgroup.closure s
hf : f ∣[k] x = f
⊢ (f ∣[k] x) ∣[k] x⁻¹ = f ∣[k] x
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
by
      simp_rw [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
      exact (f.bdd_at_cusps' hc g hg).const_smul_left (σ g (c • (1 : ℂ)))

Goal state after: