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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val

Tactic:
have he : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2 := by grind
  have hep : ∀ {x}, x ∈ Ico 1 (p / 2).succ → x < p := fun hx =>
    lt_of_le_of_lt (he hx).2 (Nat.div_lt_self hp.1.pos (by decide))
  have hpe : ∀ {x}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x := fun hx hpx =>
    not_lt_of_ge (le_of_dvd (Nat.pos_of_ne_zero (he hx).1) hpx) (hep hx)
  have hmem : ∀ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ),
      (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ := by
    intro x hx
    simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]
  have hsurj : ∀ (b : ℕ) (hb : b ∈ Ico 1 (p / 2).succ),
      ∃ x, ∃ _ : x ∈ Ico 1 (p / 2).succ, (a * x : ZMod p).valMinAbs.natAbs = b := by
    intro b hb
    refine ⟨(b / a : ZMod p).valMinAbs.natAbs, mem_Ico.mpr ⟨?_, ?_⟩, ?_⟩
    · apply Nat.pos_of_ne_zero
      simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff,
        valMinAbs_eq_zero, inv_eq_zero, Int.natAbs_eq_zero, Ne, _root_.mul_eq_zero, or_self_iff]
    · apply lt_succ_of_le; apply natAbs_valMinAbs_le
    · rw [natCast_natAbs_valMinAbs]
      split_ifs
      · rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
      · rw [mul_neg, mul_div_cancel₀ _ hap, natAbs_valMinAbs_neg, valMinAbs_def_pos,
          val_cast_of_lt (hep hb), if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]
  exact Multiset.map_eq_map_of_bij_of_nodup _ _ (Finset.nodup _) (Finset.nodup _)
    (fun x _ => (a * x : ZMod p).valMinAbs.natAbs) hmem
    (inj_on_of_surj_on_of_card_le _ hmem hsurj le_rfl) hsurj (fun _ _ => rfl)

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

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

Tactic:
· have ht' : 0 < t := hT₀.trans ht
        rw [h ht', ← mul_assoc]
        exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : ϖ ^ (n + 1) ∣ x * ϖ ^ n
⊢ x ∈ I

Tactic:
obtain ⟨y, hy⟩ := hx

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x * ϖ ^ n = ϖ ^ (n + 1) * y
⊢ x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : NeZero b
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
exact eq_zero_iff_not_coprime.2 h

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

Goal state before:
pp: a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
| legendreSym p (a % ↑p)

Tactic:
← legendreSym.mod

Goal state after:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
h₁✝ h₂ : Nat.Prime p
| legendreSym p a
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: 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' | a') = J(↑b % ↑(4 * a) % ↑a' | a')

Tactic:
Int.emod_emod_of_dvd b

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'
⊢ J(↑b % ↑a' | a') = J(↑b % ↑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'
⊢ ↑a' ∣ ↑(4 * a)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
⊢ TotallyBounded Set.univ ↔ Finite 𝓀[K]

Tactic:
by
  constructor
  · intro H
    obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
    have := Metric.finite_approx_of_totallyBounded H ‖p‖ (norm_pos_iff.mpr hp.ne_zero)
    simp only [Set.subset_univ, Set.univ_subset_iff, true_and] at this
    obtain ⟨t, ht, ht'⟩ := this
    rw [← Set.finite_univ_iff]
    refine (ht.image (IsLocalRing.residue _)).subset ?_
    rintro ⟨x⟩
    replace ht' := ht'.ge (Set.mem_univ x)
    simp only [Set.mem_iUnion, Metric.mem_ball, exists_prop] at ht'
    obtain ⟨y, hy, hy'⟩ := ht'
    simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Set.mem_univ,
      IsLocalRing.residue, Set.mem_image, true_implies]
    refine ⟨y, hy, ?_⟩
    convert!
      (Ideal.Quotient.mk_eq_mk_iff_sub_mem (I := 𝓂[K]) y x).mpr
        _
          -- TODO: make Valued.maximalIdeal abbreviations instead of def

    -- TODO: make Valued.maximalIdeal abbreviations instead of def
    rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
      (Valuation.integer.integers _).coe_span_singleton_eq_setOfPred_le_v_algebraMap]
    rw [dist_comm] at hy'
    simpa [dist_eq_norm] using! hy'.le
  · intro H
    rw [Metric.totallyBounded_iff]
    intro ε εpos
    obtain ⟨p, hp⟩ := IsDiscreteValuationRing.exists_irreducible 𝒪[K]
    have hp' := Valuation.integer.v_irreducible_lt_one hp
    obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖(p : K)‖ ^ n < ε := exists_pow_lt_of_lt_one εpos
      (toNormedField.norm_lt_one_iff.mpr hp')
    have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n
    refine ⟨Quotient.out '' (Set.univ (α := 𝒪[K] ⧸ (𝓂[K] ^ n))), Set.toFinite _, ?_⟩
    have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) := by
      ext
      simp [← norm_pow]
    simp only [Ideal.univ_eq_iUnion_image_add (𝓂[K] ^ n),
      hp.maximalIdeal_pow_eq_setOfPred_le_v_coe_pow,
      this, AddSubgroupClass.coe_norm, Set.image_univ, Set.mem_range, Set.iUnion_exists,
      Set.iUnion_iUnion_eq', Set.iUnion_subset_iff, Metric.vadd_closedBall, vadd_eq_add, add_zero]
    intro
    exact (Metric.closedBall_subset_ball hn).trans (Set.subset_iUnion_of_subset _ le_rfl)

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

Goal state before:
pp: case pos
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : γ = 0
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}

pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}

Tactic:
· simp [hγ]

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬v w ≤ ↑↑z
⊢ IsOpen {w_1 | v w_1 = v w}

Tactic:
simp_rw [← v.restrict_inj]

Goal state after:
case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬v w ≤ ↑↑z
⊢ IsOpen {w_1 | v.restrict w_1 = v.restrict w}
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:

Tactic:
_ = ‖((s - 1) * s * ∫ t in Set.Ioi 1, S t * ↑t ^ (-(s : ℂ) - 1)) -
          l * s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-(s : ℂ)))‖ := by
      rw [h₃, mul_one, mul_comm l, LSeries_eq_mul_integral _ zero_le_one (by rwa [ofReal_re])
        (hfS _ hs), neg_add', mul_assoc]
      exact isBigO_atTop_natCast_rpow_of_tendsto_div_rpow (a := l) (by simpa using hlim)
    _ = ‖(s - 1) * s * ∫ t in Set.Ioi 1, (S t * (t : ℂ) ^ (-s - 1 : ℂ) - l * t ^ (-s : ℂ))‖ := by
      rw [integral_sub, integral_const_mul]
      · congr; ring
      · exact (lemma₁ hlim hs).mono_set Set.Ioi_subset_Ici_self
      · exact (integrableOn_Ioi_cpow_of_lt
          (by rwa [neg_re, ofReal_re, neg_lt_neg_iff]) zero_lt_one).const_mul _
    _ = ‖(s - 1) * s * ∫ t in Set.Ioi 1, (S t - l * t) * (t : ℂ) ^ (-s - 1 : ℂ)‖ := by
      congr 2
      refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
      replace ht : (t : ℂ) ≠ 0 := ne_zero_of_one_lt_re ht
      rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ ht]
    _ ≤ (s - 1) * s * ∫ t in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-s - 1 : ℂ)‖ := by
      rw [norm_mul, show ((s : ℂ) - 1) * s = ((s - 1) * s : ℝ) by simp, norm_real,
        Real.norm_of_nonneg hs']
      exact mul_le_mul_of_nonneg_left (norm_integral_le_integral_norm _) hs'
    -- Next, step is to bound the integral of `‖S t - l * t‖ * t ^ (-s - 1)`.
    _ = (s - 1) * s * ∫ t in Set.Ioi 1, ‖S t - l * t‖ * t ^ (-s - 1) := by
      congr 1
      refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
      replace ht : 0 ≤ t := zero_le_one.trans ht.le
      rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg ht _)]
    -- For that, we cut the integral in two parts using `T` as the cutting point.
    _ = (s - 1) * s * (Cs + ∫ t in Set.Ioi T, ‖S t - l * t‖ * t ^ (-s - 1)) := by
      rw [← Set.Ioc_union_Ioi_eq_Ioi hT₁, setIntegral_union Set.Ioc_disjoint_Ioi_same
        measurableSet_Ioi]
      · exact h₁.mono_set <| Set.Ioc_subset_Ioi_self.trans Set.Ioi_subset_Ici_self
      · exact h₁.mono_set <| Set.Ioi_subset_Ici_self.trans <| Set.Ici_subset_Ici.mpr hT₁
    -- The first part can be bounded by `C` using `h₄`.
    _ ≤ (s - 1) * s * C + s * ((s - 1) * ∫ t in Set.Ioi T, ‖S t - l * t‖ * t ^ (-s - 1)) := by
      rw [mul_add, ← mul_assoc, mul_comm s]
      gcongr
    -- The second part is bounded using `LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂`
    -- since `‖S t - l t‖ ≤ ε * t` for all `t ≥ T`.
    _ ≤ (s - 1) * s * C + s * ε := by
      gcongr
      exact LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂ h₀ hε hs hT₁
        fun t ht ↦ (hT t ht.le).le

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inr
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : ‖(map (castRingHom ℂ) p).leadingCoeff‖ ≤ 1
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast] at ⊢ h_ineq

Goal state after:
case inr
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
h_ineq : ‖↑p.leadingCoeff‖ ≤ 1
⊢ ‖↑p.leadingCoeff‖ = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (1 + α) ^ 2 = 2 * ω

Tactic:
by
  ext <;> simp [α, ω, sq] <;> norm_num

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
⊢ 1 ^ (2 * k + 1) + (ZMod.castHom ⋯ (X q)) (3 ^ k) * α = 1 - α

Tactic:
this,

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
⊢ 1 ^ (2 * k + 1) + (ZMod.castHom ⋯ (X q)) (-1) * α = 1 - α
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
this : 2 * ((q + 1) / 2) = q + 1
⊢ (1 + α) ^ (2 * ((q + 1) / 2)) = -2

Tactic:
this,

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

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
leg : ↑(legendreSym q 2) = ↑2 ^ (q / 2)
this : 2 = ↑2
⊢ 2 ^ (q / 2) * 2 = 2

Tactic:
this,

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
leg : ↑(legendreSym q 2) = ↑2 ^ (q / 2)
this : 2 = ↑2
⊢ ↑2 ^ (q / 2) * ↑2 = ↑2
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) = 2 * -1
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
refine (IsUnit.of_mul_eq_one (M := X q) ↑((q + 1) / 2) ?_).mul_left_cancel this

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) = 2 * -1
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ 2 * ↑((q + 1) / 2) = 1
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
apply orderOf_dvd_iff_pow_eq_one.2
    apply Units.ext
    push_cast
    exact ω_pow_eq_one p' h

Goal state after:
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 ↥⊥

Tactic:
exact Subsingleton.discreteTopology

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

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

Tactic:
apply relIndex_inf_ne_zero

Goal state after:
case left.hH
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ.relIndex (mapGL ℝ).range ≠ 0

case hK
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ'.relIndex (mapGL ℝ).range ≠ 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g

Tactic:
have : 0 < Fintype.card ι := Fintype.card_pos
  simpa [← zpow_natCast, this] using ModularForm.prod_slash (s := (.univ : Finset ι))

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
this,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ f z * denom γ ↑z ^ k = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ cd ∈ (fun g ↦ ↑g 1) '' Set.univ

Tactic:
have det_A_1 : det A = 1 := by
    convert! gcd_eqn
    rw [det_fin_two]
    simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ cd ∈ (fun g ↦ ↑g 1) '' Set.univ
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ 𝒢.strictWidthInfty

Tactic:
by
  unfold strictWidthInfty; aesop

Goal state after:
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✝
⊢ ((c • ⇑f) ∣[k] g) =O[atImInfty] 1

Tactic:
← smul_one_smul ℂ c ⇑f,

Goal state after:
Γ : 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✝
⊢ (((c • 1) • ⇑f) ∣[k] g) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((c • ⇑f) ∣[k] g) atImInfty (𝓝 0)

Tactic:
← smul_one_smul ℂ c ⇑f,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℝ
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto (((c • 1) • ⇑f) ∣[k] g) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto ((c • ⇑f) ∣[k] g) atImInfty (𝓝 0)

Tactic:
← smul_one_smul ℂ c ⇑f,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : CuspForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ Filter.Tendsto (((c • 1) • ⇑f) ∣[k] g) atImInfty (𝓝 0)
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
⊢ IsBoundedAtImInfty (⇑f ∣[k] g)

Tactic:
rw [← OnePoint.isBoundedAt_infty_iff, SL_slash, ← 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.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
obtain ⟨a, ha, ha'⟩ := exists_between hb

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
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‖
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
simp only [Real.norm_rpow_of_nonneg (_ : ℍ).im_pos.le,
      Real.norm_of_nonneg (_ : ℍ).im_pos.le] at hy

Goal state after:
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
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
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 τ)
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

Tactic:
have H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (.ofScalars ℂ c) 0 1 :=
    hasFPowerSeriesOnBall_update hh hf

Goal state after:
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
⊢ HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
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 τ
F : ℝ
hF𝒟 : ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
refine ⟨F, fun τ ↦ ?_⟩

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
τ : ℍ
⊢ ‖f τ‖ ≤ F * max τ.im (1 / τ.im) ^ t