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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction (𝓕 Φ) s = ∑ j, Φ j * expZeta (toAddCircle (-j)) s

Tactic:
have (j : ZMod N) : Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s =
      Φ j * expZeta (toAddCircle (-j)) s := by
    by_cases h : -j ≠ 0 ∨ s ≠ 1
    · rw [LFunction_stdAddChar_eq_expZeta _ _ h]
    · simp only [neg_ne_zero, not_or, not_not] at h
      rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
this : ∀ (j : ZMod N), Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
⊢ LFunction (𝓕 Φ) s = ∑ j, Φ j * expZeta (toAddCircle (-j)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k + 1)! = ↑((2 * k + 1) * (2 * k)!)

Tactic:
← Nat.factorial_succ

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k + 1)! = ↑(2 * k + 1)!
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
by positivity

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

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 0 * completedHurwitzZetaEven (toAddCircle 0) s = Φ 1 * completedRiemannZeta s

Tactic:
map_zero,

Goal state after:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 0 * completedHurwitzZetaEven 0 s = Φ 1 * completedRiemannZeta s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e'_2
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))

Tactic:
rw [← Nat.cast_two, ← Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one (by lia)]
    simp [push_cast]

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

Goal state before:
pp: case e'_2
⊢ riemannZeta 4 = ↑(∑' (b : ℕ), 1 / ↑b ^ 4)

Tactic:
← Nat.cast_one,

Goal state after:
case e'_2
⊢ riemannZeta 4 = ↑(∑' (b : ℕ), ↑1 / ↑b ^ 4)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * ↑((-1) ^ (k + 1) * bernoulli' (k + 1)) / (↑k + 1)

Tactic:
Rat.cast_mul,

Goal state after:
k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * (↑((-1) ^ (k + 1)) * ↑(bernoulli' (k + 1))) / (↑k + 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ k ≠ 0

Tactic:
by positivity

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ 0 ≤ ↑n ^ (-x)

Tactic:
by positivity

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ 0 ≤ ↑↑p ^ (-s).re

Tactic:
by positivity

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
x✝ : Nat.Primes × ℕ
⊢ 0 x✝ ≤ (↑↑x✝.1)⁻¹ ^ x✝.2 * (↑↑x✝.1)⁻¹ ^ (3 / 2)

Tactic:
by positivity

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
| Summable fun x ↦ ∑' (y : ℕ), (↑↑x)⁻¹ ^ y * (↑↑x)⁻¹ ^ (3 / 2)

Tactic:
enter [1, p]; rw [tsum_mul_right, tsum_geometric_of_lt_one (hp₀ p).le (hp₁ p)]

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
| (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ (fun x ↦ LFunctionTrivChar N (1 + ↑x)) =O[𝓝[>] 0] fun x ↦ 1 / ↑x

Tactic:
have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by
    have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
    exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ
  exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
⊢ LFunction χ (1 + I * ↑t) ≠ 0

Tactic:
intro Hz
  have hz₁ : t ≠ 0 ∨ χ ≠ 1 := by
    refine h.symm.imp_right (fun h H ↦ ?_)
    simp only [H, one_pow, ne_eq, not_true_eq_false] at h
  have hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1 :=
    h.symm.imp_left <| mul_ne_zero two_ne_zero
  have help (x : ℝ) : ((1 / x) ^ 3 * x ^ 4 * 1 : ℂ) = x := by
    rcases eq_or_ne x 0 with rfl | h
    · rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
    · rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]
  -- put together the various `IsBigO` statements and `norm_LFunction_product_ge_one`
  -- to derive a contradiction
  have H₀ : (fun _ : ℝ ↦ (1 : ℝ)) =O[𝓝[>] 0]
      fun x ↦ LFunctionTrivChar N (1 + x) ^ 3 * LFunction χ (1 + x + I * t) ^ 4 *
                   LFunction (χ ^ 2) (1 + x + 2 * I * t) :=
    IsBigO.of_bound' <| eventually_nhdsWithin_of_forall
      fun _ hx ↦ (norm_one (α := ℝ)).symm ▸ (χ.norm_LFunction_product_ge_one hx t).le
  have H := (LFunctionTrivChar_isBigO_near_one_horizontal (N := N)).pow 3 |>.mul <|
    (χ.LFunction_isBigO_horizontal_of_eq_zero hz₁ Hz).pow 4 |>.mul <|
    LFunction_isBigO_horizontal _ hz₂
  simp only [ofReal_mul, ofReal_ofNat, mul_left_comm I, ← mul_assoc, help] at H
  -- go via absolute value to translate into a statement over `ℝ`
  replace H := (H₀.trans H).norm_right
  simp only [norm_real] at H
  exact isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
    H.of_norm_right.trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
⊢ ∀ (k : ℕ), ‖F y' k‖ ≤ ‖F y k‖

Tactic:
k

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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
⊢ ‖F y' k‖ ≤ ‖F y k‖
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case inl
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖f k‖ / (↑k / ‖↑n + 1‖) ^ y' ≤ ‖f k‖ / (↑k / ‖↑n + 1‖) ^ y

Tactic:
← Nat.cast_one,

Goal state after:
case inl
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖f k‖ / (↑k / ‖↑n + ↑1‖) ^ y' ≤ ‖f k‖ / (↑k / ‖↑n + ↑1‖) ^ y
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ 0 < ↑(n + 1)

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I) =
    ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one, ← div_div, div_I,
      div_mul_eq_mul_div₀]

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) * I / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
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
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ f 0 + ∑ x ∈ Icc (0 + 1) n, f x = ∑ k ∈ Icc 1 n, f k

Tactic:
hf,

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ 0 + ∑ x ∈ Icc (0 + 1) n, f x = ∑ k ∈ Icc 1 n, f k
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)) ↔
    IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)

Tactic:
constructor
  · rintro ⟨e⟩
    let x := e.symm (exp (-1))
    have hx0 : x ≠ 0 := by simp [x]
    have hx1 : x < 1 := by simp [-exp_neg, x, ← lt_map_inv_iff, ← exp_zero]
    refine ⟨⟨x, hx1, fun y hy ↦ ?_⟩, ⟨x, hx0, hx1.ne⟩, .comap e.toMonoidHom e.strictMono⟩
    rcases eq_or_ne y 0 with rfl | hy0
    · simp
    · rw [← map_one e.symm, ← map_inv_lt_iff, ← log_lt_log (by simp [hy0]) (by simp)] at hy
      rw [← map_inv_le_iff, ← log_le_log (by simp [hy0]) (by simp)]
      simp only [OrderMonoidIso.equivLike_inv_eq_symm, OrderMonoidIso.symm_symm, log_one,
        log_exp] at hy ⊢
      linarith
  · rintro ⟨hD, hN, hM⟩
    rw [isNontrivial_iff_nontrivial_units] at hN
    rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
    intro H
    obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element
    obtain ⟨y, hy, hy'⟩ := exists_between hx
    exact hy.not_ge (hx' y hy')

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
⊢ Odd (mersenne (p + 1)) ↔ p + 1 ≠ 0

Tactic:
simpa using! Nat.Even.sub_odd (one_le_pow₀ one_le_two)
      (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ p ≠ 0

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: 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 < n

Tactic:
calc
    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.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ 2 * ⌊↑(n.choose ↑i) * ↑B⌋ + 1

Tactic:
by positivity

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 0 ≤ ↑(n.choose ↑i) * ↑B

Tactic:
by positivity

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

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ Γ.HasDetPlusMinusOne

Tactic:
rw [hasDetPlusMinusOne_iff_abs_det]

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ ∀ {g : GL (Fin 2) ℝ}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
this : GeneralLinearGroup.det (g ^ n) = 1
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1

Tactic:
map_pow

Goal state after:
n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
t : SL(2, ℤ)
ht : (mapGL ℝ) t = g ^ n
this : GeneralLinearGroup.det g ^ n = 1
⊢ |↑(GeneralLinearGroup.det g ^ n)| = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℝ
x : SL(2, ℤ)
⊢ x ∈ conjGL Γ g ↔
    ∃ y ∈ Γ,
      toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        g * toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) x) * g⁻¹

Tactic:
simp [conjGL, mapGL, Subgroup.mem_inv_pointwise_smul_iff, toConjAct_smul]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
⊢ g * (mapGL ℚ) ⟨y, hy⟩ * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
obtain ⟨k, hk⟩ : ∃ k, y = 1 + (a₁ * a₂ * M) • k := by
    replace hy' : y.map (Int.cast : ℤ → ZMod (a₁ * a₂ * M)) = 1 := by
      rw [CongruenceSubgroup.Gamma_mem', Subtype.ext_iff] at hy'
      simpa using! hy'
    use Matrix.of fun i j ↦ (y - 1) i j / (a₁ * a₂ * M)
    rw [← sub_eq_iff_eq_add']
    ext i j
    simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]
    refine (Int.mul_ediv_cancel_of_dvd ?_).symm
    rw [← Matrix.map_one Int.cast (by simp) (by simp), ← sub_eq_zero,
      ← Matrix.map_sub _ (by simp)] at hy'
    simpa only [Matrix.zero_apply, Matrix.map_apply, ZMod.intCast_zmod_eq_zero_iff_dvd,
      Nat.cast_mul] using! congr_fun₂ hy' i j

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
⊢ g * (mapGL ℚ) ⟨y, hy⟩ * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
h : ![↑g 0 0, ↑g 1 0] = 0
⊢ False

Tactic:
by
      simpa [det_fin_two, show g 0 0 = 0 from congr_fun h 0, show g 1 0 = 0 from congr_fun h 1]
        using g.det_ne_zero

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

Goal state before:
pp: case mpr
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
b : IsZeroAtImInfty (f ∣[k] γ)
hc : IsCusp ((mapGL ℝ) γ • ∞) (mapGL ℝ).range
⊢ ((mapGL ℝ) γ • ∞).IsZeroAt f k

Tactic:
simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using! b

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
⊢ f = 0

Tactic:
by
  ext z
  have hf := slash_action_eqn'' f h_neg_one z
  rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf
  have h2 : (2 : ℂ) * f z = 0 := by linear_combination hf
  exact (mul_eq_zero.mp h2).resolve_left (by norm_num)

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
this : (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) = f
⊢ Tendsto f atImInfty (𝓝 (cuspFunction h f 0))

Tactic:
simpa [this] using hfanalytic.continuousAt.tendsto.comp (qParam_tendsto_atImInfty hh)

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
τ : ℍ
⊢ τ.im ^ t ≠ 0

Tactic:
by positivity

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

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : y ≤ τ.im
⊢ 0 ≤ τ.im ^ t

Tactic:
by positivity

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

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      f UpperHalfPlane.I
h2I2 :
  f
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) •
        ⟨2, ⋯⟩ • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S))
          ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^
        k *
      f (⟨2, ⋯⟩ • UpperHalfPlane.I)
⊢ k = 0 ∨ c = 0

Tactic:
hf,

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
this : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(1)) k
hI :
  Function.const ℍ c
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑UpperHalfPlane.I ^
        k *
      Function.const ℍ c UpperHalfPlane.I
h2I2 :
  Function.const ℍ c
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S) •
        ⟨2, ⋯⟩ • UpperHalfPlane.I) =
    denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S))
          ↑(⟨2, ⋯⟩ • UpperHalfPlane.I) ^
        k *
      Function.const ℍ c (⟨2, ⋯⟩ • UpperHalfPlane.I)
⊢ k = 0 ∨ c = 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
this : update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝 0] cuspFunction h f
⊢ c 0 = cuspFunction h f 0

Tactic:
simpa [update_self] using this.eq_of_nhds

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

Goal state before:
pp: E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ 0 < τ.im ^ t

Tactic:
by positivity

Goal state after: