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

Goal state before:
pp: case refine_2
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
h : span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)} = ⊥
⊢ False

Tactic:
exact (show Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0 from
      Polynomial.map_monic_ne_zero (minpoly.monic hx')) (span_singleton_eq_bot.mp h)

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C,
    ∀ {a b c d : K},
      ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

Tactic:
obtain ⟨C', hC₀, hC⟩ := mulHeight_sym2_ge K
  refine ⟨log C', fun hab hcd ↦ ?_⟩
  simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact log_le_log (by positivity) (hC hab hcd)

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

Goal state before:
pp: case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
have h' : Continuous fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ p * ↑p ^ (-s)) :=
      (differentiable_LFunction h).continuous.mul <| continuous_finsetProd _ fun p hp ↦ by
        have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
        fun_prop

Goal state after:
case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
h' : Continuous fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
by
  rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]
  split_ifs with h
  · rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]
    push_cast; ring
  · rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∀ k_1 < m, IntervalIntegrable (bernoulliFun (k + 1)) volume (↑k_1 / ↑m) (↑(k_1 + 1) / ↑m)

Tactic:
intros; exact Continuous.intervalIntegrable (by fun_prop) _ _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∀ i ∈ Finset.range m, IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0 (↑m)⁻¹

Tactic:
intros; exact Continuous.intervalIntegrable (by fun_prop) _ _

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

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

Tactic:
rw [riemannZeta_neg_nat_eq_bernoulli', bernoulli, Rat.cast_mul, Rat.cast_pow, Rat.cast_neg,
    Rat.cast_one, ← neg_one_mul, ← mul_assoc, pow_succ, ← mul_assoc, ← mul_pow, neg_one_mul (-1),
    neg_neg, one_pow, one_mul]

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

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

Tactic:
div_eq_mul_inv

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

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

pp: case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k)

Tactic:
· skip

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
⊢ 0 ≤
    3 * (-log (1 - 1 ↑n * ↑n ^ (-↑x))).re + 4 * (-log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y)))).re +
      (-log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)))).re

Tactic:
by_cases hn' : IsUnit (n : ZMod N)
  · have hn : (n : ℝ) ^ (-x) < 1 := by
      rw [Real.rpow_neg (Nat.cast_nonneg n), inv_lt_one_iff₀]
      exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx
    have hz : ‖χ n * (n : ℂ) ^ (-(I * y))‖ = 1 := by
      rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]
      simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
        neg_zero, Real.rpow_zero, one_mul]
    rw [MulChar.one_apply hn', one_mul]
    convert! re_log_comb_nonneg' (by positivity) hn hz using 6
    · simp only [ofReal_cpow n.cast_nonneg (-x), ofReal_natCast, ofReal_neg]
    · congr 2
      rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, mul_left_comm]
    · rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]
  · simp only [MulChar.map_nonunit _ hn', zero_mul, sub_zero, log_one, neg_zero, zero_re, mul_zero,
      neg_add_rev, add_zero, pow_two, le_refl]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : AnalyticOnNhd ℂ F Set.univ
hG : AnalyticOnNhd ℂ G Set.univ
this : {z | 1 < z.re} ∈ 𝓝 2
hFG : F =ᶠ[𝓝 2] G
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s

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

Goal state before:
pp: q : ℕ
a : ZMod q
⊢ (Function.support fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n) = {p | Nat.Prime p ∧ ↑p = a}

Tactic:
by
  simp only [Function.support, ne_eq, div_eq_zero_iff, ite_eq_right_iff,
    Set.indicator_apply_eq_zero, Set.mem_ofPred_eq, Nat.cast_eq_zero, not_or, Classical.not_imp]
  ext1 p
  simp only [Set.mem_ofPred_eq]
  exact ⟨fun H ↦ ⟨H.1.1, H.1.2.1⟩,
    fun H ↦ ⟨⟨H.1, H.2, vonMangoldt_ne_zero_iff.mpr H.1.isPrimePow⟩, H.1.ne_zero⟩⟩

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)

pp: case a.a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
| I ^ (2 * k + 1)

Tactic:
· skip

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

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s

Tactic:
exact LSeries.eq_zero_of_not_LSeriesSummable f s <| mt LSeriesSummable.abscissaOfAbsConv_le <|
    h ▸ fun H ↦ (H.trans_lt <| EReal.coe_lt_top _).false

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

pp: case a
k : ℕ
hk : k ≠ 0
| 2

Tactic:
· skip

Goal state after:
case a
k : ℕ
hk : k ≠ 0
| 2
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
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
⊢ (fun n ↦ if n = 0 then 0 else f n) =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop 0] with n h using if_neg h

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) * ↑(p / 2)!

Tactic:
simpa using gauss_lemma_aux₁ p hap

Goal state after:
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
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
⊢ 0 < t → ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Tactic:
ht'

Goal state after:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
ht' : 0 < t
⊢ ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖
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:
by
  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.Topology.Algebra.Module.Compact

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ IsCompact ↑(Fintype.linearCombination R Subtype.val).range

Tactic:
refine isCompact_range ?_

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ Continuous ⇑(Fintype.linearCombination R Subtype.val)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J((n :: l').prod | n✝) = (J(n | n✝) :: List.map (fun a ↦ J(a | n✝)) l').prod

Tactic:
List.prod_cons,

Goal state after:
case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n * l'.prod | n✝) = (J(n | n✝) :: List.map (fun a ↦ J(a | n✝)) l').prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n * l'.prod | n✝) = (J(n | n✝) :: List.map (fun a ↦ J(a | n✝)) l').prod

Tactic:
List.prod_cons,

Goal state after:
case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n * l'.prod | n✝) = J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | (n :: l').prod) = (J(a | n) :: List.map (fun n ↦ J(a | n)) l').prod

Tactic:
List.prod_cons,

Goal state after:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | n * l'.prod) = (J(a | n) :: List.map (fun n ↦ J(a | n)) l').prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | n * l'.prod) = (J(a | n) :: List.map (fun n ↦ J(a | n)) l').prod

Tactic:
List.prod_cons,

Goal state after:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | n * l'.prod) = J(a | n) * (List.map (fun n ↦ J(a | n)) l').prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Nat.gcd 2 b = 1

Tactic:
← b.mod_add_div 2,

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ Nat.gcd 2 (b % 2 + 2 * (b / 2)) = 1
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] ⧸ ⊤)

Tactic:
exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (ω ^ 2 ^ (p' + 1)) ^ 2 = (-1) ^ 2

Tactic:
ω_pow_eq_neg_one p' h

Goal state after:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ (-1) ^ 2 = (-1) ^ 2
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inl
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
ha : 1 ≤ 1
⊢ DiscreteTopology ↥(zpowers 1)

pp: case inr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
· rw [zpowers_one_eq_bot]
    exact Subsingleton.discreteTopology

Goal state after:
case inr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
⊢ DiscreteTopology ↥(zpowers g)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ IsCongruenceSubgroup (Gamma1 N)

Tactic:
refine ⟨N, NeZero.ne _, fun A hA ↦ ?_⟩

Goal state after:
N : ℕ
inst✝ : NeZero N
A : SL(2, ℤ)
hA : A ∈ Γ(N)
⊢ A ∈ Gamma1 N
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case e'_1
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ↔ GeneralLinearGroup.det (-g) = -1

Tactic:
simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

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

Goal state before:
pp: case e'_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = -1 ↔ GeneralLinearGroup.det (-g) = 1

Tactic:
simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
inst✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
by
      rw [← smul_one_smul ℂ]
      simp [-smul_assoc, smul_slash, slash_action_eqn _ _ hγ, σ, Subgroup.HasDetOne.det_eq hγ]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
⊢ Tendsto (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop

Tactic:
have :
    (fun p : Fin 2 → ℤ => normSq ((p 0 : ℂ) * ↑z + ↑(p 1))) =
      normSq ∘ f ∘ fun p : Fin 2 → ℤ => ((↑) : ℤ → ℝ) ∘ p := by
    ext1
    rw [f_def]
    dsimp only [Function.comp_def]
    rw [ofReal_intCast, ofReal_intCast]

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
⊢ Tendsto (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ (⇑f ∘ ↑ofComplex) (w + ↑h) = (⇑f ∘ ↑ofComplex) w

Tactic:
have : im (w + h) ≤ 0 := by simpa using hw
    simp [ofComplex_apply_of_im_nonpos this, ofComplex_apply_of_im_nonpos hw]

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ ∞.IsBoundedAt (⇑f ∣[k] (g * γ)) ?m.67

pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ ℤ

Tactic:
← OnePoint.IsBoundedAt.smul_iff

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ ((g * γ) • ∞).IsBoundedAt (⇑f) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ∞.IsBoundedAt (⇑f ∣[k] toGL ((map (Int.castRingHom ℝ)) g)) ?m.26

pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ℤ

Tactic:
← OnePoint.IsBoundedAt.smul_iff

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ (toGL ((map (Int.castRingHom ℝ)) g) • ∞).IsBoundedAt (⇑f) k
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 : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
obtain ⟨F, hF𝒟⟩ : ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t :=
    exists_bound_fundamental_domain_of_isBigO hf_cont hf_infinity

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: x : ℕ+ × ℕ+
⊢ (↑x.1, ↑x.2) ∈ (↑⟨↑x.1 * ↑x.2, ⋯⟩).divisorsAntidiagonal

Tactic:
simp [Nat.mem_divisorsAntidiagonal]

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ C / τ.im ^ (↑k / 2) = C * (τ.im ^ (↑k / 2))⁻¹

Tactic:
div_eq_mul_inv

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
τ : ℍ
⊢ C * (τ.im ^ (↑k / 2))⁻¹ = C * (τ.im ^ (↑k / 2))⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤
      rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) by
    calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]

Goal state after:
τ : ℂ
hτ : 0 < τ.im
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt]

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)
⊢ ∀ (x : Πʳ (i : ι), [R i, A i] × Y), Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n

Tactic:
← Int.natCast_dvd_natCast,

Goal state after:
case inl
x y : ℕ
hxy : ↑2 ∣ ↑(x - y)
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 =
    emultiplicity (↑2) (↑x + ↑y) + emultiplicity (↑2) (↑x - ↑y) + emultiplicity 2 n