mathlib-initiative/mathlib-tactics huggingface dataset:
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
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x 1 ∪ Set.Icc 1⁻¹ y⁻¹⁻¹

Tactic:
inv_one,

Goal state after:
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
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x 1 ∪ Set.Icc 1 y⁻¹⁻¹
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
h

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

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

Tactic:
h

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

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
| (aeval (ψ y)) p

Tactic:
← map_id (p := p)

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
| (aeval (ψ y)) (map (RingHom.id ℤ) p)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ ↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0

Tactic:
h

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ ↑0 = 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetPlusMinusOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1 ∨ GeneralLinearGroup.det h = -1

Tactic:
simpa [ConjAct.smul_def] using HasDetPlusMinusOne.det_eq hh

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

Goal state before:
pp: N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

Tactic:
by
  constructor
  · intro ha
    have adet : (A.1.1.det : ZMod N) = 1 := by simp only [A.1.property, Int.cast_one]
    rw [Matrix.det_fin_two] at adet
    simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul] at *
    simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul, ha, Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero,
      sub_zero] using adet
  · intro ha
    simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk]
    exact ha.2.1

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

Goal state before:
pp: N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Γ(N) = Γ(N)

Tactic:
by
  apply Subgroup.Normal.conjAct (Gamma_normal N)

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

Goal state before:
pp: case inr
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 ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
by_cases hn : Even (Fintype.card n)
    · convert! HasDetPlusMinusOne.det_eq hg using 1 <;>
        simp [Units.ext_iff, det_neg, hn]
    · convert! (HasDetPlusMinusOne.det_eq hg).symm using 1 <;>
        simp [Units.ext_iff, det_neg, Nat.not_even_iff_odd.mp hn, neg_eq_iff_eq_neg]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c

Tactic:
· rw [coe_eq_coe, div_eq_iff h]
    grind

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

Goal state before:
pp: A : SL(2, ℤ)
x : ℂ
⊢ Function.const ℍ x ∣[0] A = Function.const ℍ x

Tactic:
funext
  simp [SL_slash, slash_def, σ, zero_lt_one]

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

Goal state before:
pp: ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * ↑(#s) = #s • k

Tactic:
nsmul_eq_mul'

Goal state after:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * ↑(#s) = k * ↑(#s)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: N : ℕ
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictPeriods = AddSubgroup.zmultiples ↑N

Tactic:
ext x
  have : AddSubgroup.zmultiples ↑N = .map (Int.castAddHom ℝ) (.zmultiples N) := by simp
  simp only [this, mem_strictPeriods_iff, Subgroup.mem_map, Gamma_mem]
  constructor
  · rintro ⟨g, ⟨-, hg, -, -⟩, hx⟩
    rw [show x = g 0 1 by simpa using congr_arg (· 0 1) hx.symm]
    apply AddSubgroup.mem_map_of_mem
    rwa [Int.mem_zmultiples_iff, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
  · simp only [AddSubgroup.mem_map, AddSubgroup.mem_zmultiples_iff, existsAndEq, true_and,
      Units.ext_iff, mapGL_coe_matrix, map_apply_coe, forall_exists_index]
    refine fun a ha ↦ ⟨ModularGroup.T ^ (a * N), by simp [ModularGroup.coe_T_zpow], ?_⟩
    ext i j
    fin_cases i <;> fin_cases j <;> simp [ModularGroup.coe_T_zpow, ← ha]

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

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

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 : 0 < im (w + h) := by simp [hw]
    simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]
    convert! SlashInvariantForm.vAdd_apply_of_mem_strictPeriods f ⟨w, hw⟩ hΓ using 2
    ext
    simp [add_comm]

Goal state after:
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
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ (Fin 2 → ℝ) ≃ₗ[ℝ] Fin 2 → ℝ

Tactic:
by
      refine
        LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
          (GeneralLinearGroup.toLin (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) ?_))
      norm_cast
      rw [neg_sq]
      exact hcd.sq_add_sq_ne_zero

Goal state after:
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
f' : F'
h_bd : IsZeroAtImInfty ⇑f'
⊢ ∃ a > 0, petersson k ⇑f ⇑f' =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
obtain ⟨a, ha, ha'⟩ := h_bd.petersson_exp_decay_left k Γ f
  exact ⟨a, ha, .of_norm_left <| ha'.norm_left.congr_left <| petersson_norm_symm k f f'⟩

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
⊢ ∀ (γ : SL(2, ℤ)), f ∣[k] γ = f

Tactic:
intro γ

Goal state after:
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ f ∣[k] γ = f
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ finGcdMap (v ᵥ* ↑A) = r

Tactic:
have hvr : v = r • (v / r) := by
    ext i
    refine Eq.symm (Int.mul_ediv_cancel' ?_)
    fin_cases i <;> simp [← hab, Int.gcd_dvd_left, Int.gcd_dvd_right]
  rw [hvr, smul_vecMul]
  simpa using finGcdMap_smul r (Int.isCoprime_iff_gcd_eq_one.mp ((finGcdMap_div v hab).vecMulSL A))

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ^ 2 ≤ (√C * max 1 (1 / τ.im ^ ↑k)) ^ 2

Tactic:
mul_pow,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ^ 2 ≤ √C ^ 2 * max 1 (1 / τ.im ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ ∫ (x : ℝ) in 0..h, ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
let F (x : ℝ) : ℝ := ‖1 / ↑h * (1 / 𝕢 h ((x : ℂ) + 1 / n * I) ^ n
      * f ⟨(x : ℂ) + 1 / n * Complex.I, by simp [hn]⟩)‖

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
⊢ ∫ (x : ℝ) in 0..h, ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
hg',

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : (T ^ ↑g 0 0 * S) • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ ∀ (γ : SL(2, ℤ)), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c → IsZeroAtImInfty (⇑f ∣[k] γ)

Tactic:
intro γ

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c → IsZeroAtImInfty (⇑f ∣[k] γ)
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoBotOrder α
inst✝ : NoTopOrder α
⊢ Tendsto (fun p ↦ Ioo p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_gt_atTop i)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A : SL(2, ℤ)
⊢ D2 A ∣[2] A⁻¹ = -D2 A⁻¹

Tactic:
simpa [eq_neg_iff_add_eq_zero] using (D2_mul A A⁻¹).symm

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

Goal state before:
pp: case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

Tactic:
exact fun x hx ↦ mul_ne_zero (by simp [sqrt, ne_zero ⟨x, hx⟩]) (eta_ne_zero hx)

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

Goal state before:
pp: c✝ : OnePoint ℝ
hc : IsCusp c✝ (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro γ

Goal state after:
c✝ : OnePoint ℝ
hc : IsCusp c✝ (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T⁻¹ * S * T⁻¹) 1 0
hc : ↑(T⁻¹ * S * T⁻¹) 1 0 = 1
hd : ↑(T⁻¹ * S * T⁻¹) 1 1 = -1
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1

Tactic:
show T⁻¹ * S * T⁻¹ = ⟨!![-1, 0; 1, -1], by simp⟩ by decide

Goal state after:
case inr.inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T⁻¹ * S * T⁻¹) 1 0
hc : ↑(T⁻¹ * S * T⁻¹) 1 0 = 1
hd : ↑(T⁻¹ * S * T⁻¹) 1 1 = -1
hz : 1 +ᵥ ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ⟨!![-1, 0; 1, -1], ⋯⟩)) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro γ

Goal state after:
k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Summable fun m ↦ ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
rw [← summable_pnat_iff_summable_succ (f := fun b ↦ ∑' c : ℕ+, c * 𝕢 z ^ (b * c : ℕ))]

Goal state after:
z : ℍ
this :
  -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n =
    ∑' (m : ℕ), -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)
⊢ Summable fun x ↦ ∑' (c : ℕ+), ↑↑c * cexp (2 * ↑π * I * ↑z) ^ (↑x * ↑c)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ E2 z = 1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
by
  simp [E2, G2_eq_tsum_cexp, riemannZeta_two]
  field

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
apply (summable_pow_mul_cexp k 1 z).congr
    simp

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬(-I * ↑τ = 0 ∧ 1 / 2 ≠ 0)

Tactic:
not_and_or

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬-I * ↑τ = 0 ∨ ¬1 / 2 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
have HE2 := tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries hk z

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ (1 / 2) • ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z =
    1 +
      (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        (-2 * ↑π * I) ^ (2 * (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))

Tactic:
mul_pow,

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2 * ↑π) ^ (2 * (m + 1)) * I ^ (2 * (m + 1))) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2 * ↑π) ^ (2 * (m + 1)) * I ^ (2 * (m + 1))) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))

Tactic:
mul_pow,

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        ((-2) ^ (2 * (m + 1)) * ↑π ^ (2 * (m + 1)) * I ^ (2 * (m + 1))) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case hbc
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ ↑((σ (k - 1)) n) ≤ ↑n ^ k

Tactic:
exact_mod_cast (ArithmeticFunction.sigma_le_pow_succ (k - 1) n).trans_eq (by congr 1; omega)

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝ : (i : ι) → TopologicalSpace (R i)
𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ Continuous[topologicalSpace R A 𝓖, topologicalSpace R A 𝓕] (inclusion R A h)

Tactic:
by
  simp_rw [continuous_iff_coinduced_le, topologicalSpace, coinduced_iSup, coinduced_compose]
  exact iSup₂_le fun S hS ↦ le_iSup₂_of_le S (le_trans h hS) le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]
  rw [← Int.natCast_dvd_natCast] at hxy hx
  push_cast at *
  exact Int.emultiplicity_pow_add_pow hp hp1 hxy hx hn

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Tactic:
by
  have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
  have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
  have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
  rcases n with - | n
  · simp only [pow_zero, sub_self, emultiplicity_zero, Int.ofNat_zero, add_top]
  have h : FiniteMultiplicity 2 n.succ := Nat.finiteMultiplicity_iff.mpr ⟨by simp, n.succ_pos⟩
  simp only [Nat.succ_eq_add_one] at h
  rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
  rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
  · norm_cast
    rw [h.emultiplicity_eq_multiplicity]
  · exact Int.prime_two
  · simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow
  · simpa only [even_iff_two_dvd, ← Int.not_even_iff_odd] using hx_odd.pow
  norm_cast
  contrapose hpn
  rw [pow_succ]
  conv_rhs => rw [hk]
  exact mul_dvd_mul_left _ hpn

Goal state after: