mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x ∈ IsLocalRing.maximalIdeal ↥v.integer, ¬x = 0

Tactic:
IsLocalRing.notMem_maximalIdeal.not_right,

Goal state after:
K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x, ¬IsUnit x ∧ ¬x = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y : X q
h₁ : x.1 = y.1
h₂ : x.2 = y.2
⊢ x = y

Tactic:
by
  cases x; cases y; congr

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: 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))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ 0 < ∏ p ∈ (f i / (f i).gcd (f j)).primeFactors, p ∧ ∏ p ∈ (f i / (f i).gcd (f j)).primeFactors, p < n

Tactic:
prod_primeFactors_of_squarefree <| hf'' _ hi _

Goal state after:
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))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ 0 < f i / (f i).gcd (f j) ∧ f i / (f i).gcd (f j) < n
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q k : ℕ
ih : sModNatAux (4 % q) q k = sModNat q k
⊢ sModNatAux (4 % q) q (k + 1) = sModNat q (k + 1)

Tactic:
sModNatAux,

Goal state after:
case succ
q k : ℕ
ih : sModNatAux (4 % q) q k = sModNat q k
⊢ (sModNatAux (4 % q) q k ^ 2 + (q - 2)) % q = sModNat q (k + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q k = sModNatAux b q (k + 1)

Tactic:
sModNatAux

Goal state after:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q (k + 1) = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q

Tactic:
sModNatAux,

Goal state after:
case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ (sModNatAux ((b ^ 2 + (q - 2)) % q) q k ^ 2 + (q - 2)) % q = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ (((sModNatAux b q k ^ 2 + (q - 2)) % q) ^ 2 + (q - 2)) % q = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q

Tactic:
sModNatAux

Goal state after:
case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ (((sModNatAux b q k ^ 2 + (q - 2)) % q) ^ 2 + (q - 2)) % q =
    (((sModNatAux b q k ^ 2 + (q - 2)) % q) ^ 2 + (q - 2)) % q
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H

Tactic:
have := H.dense_or_cyclic

Goal state after:
case mpr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, H = closure {a}
⊢ DiscreteTopology ↥H → ∃ g, zpowers g = H
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
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
this : ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint
⊢ g • ↑c = ↑c ↔ ↑c = g.parabolicFixedPoint

Tactic:
simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
⊢ f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B

Tactic:
ext1 τ

Goal state after:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (f ∣[k] (A * B)) τ = ((f ∣[k] A) ∣[k] B) τ
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f + g) ∣[k] A = f ∣[k] A + g ∣[k] A

Tactic:
ext1 τ

Goal state after:
k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
τ : ℍ
⊢ ((f + g) ∣[k] A) τ = (f ∣[k] A + g ∣[k] A) τ
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

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

Tactic:
zpow_one

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

case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| ≠ 0 ∨ 1 + (↑(#t) - 1) ≠ 0 ∨ 1 = 0 ∧ ↑(#t) - 1 = 0
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
⊢ IsBoundedAtImInfty ((⇑f ∣[k] g) ∣[k] γ)

Tactic:
← SlashAction.slash_mul,

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
⊢ IsBoundedAtImInfty (⇑f ∣[k] (g * γ))
Module: Mathlib.NumberTheory.ModularForms.Basic

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

Tactic:
← SlashAction.slash_mul,

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

Goal state before:
pp: case inr
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
⊢ ‖f τ‖ ≤ max D E * τ.im ^ t

Tactic:
rw [← div_le_iff₀ (by positivity)]

Goal state after:
case inr
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
⊢ ‖f τ‖ / τ.im ^ t ≤ max D E
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f) (⇑f') (g • τ)) atImInfty (𝓝 0)

Tactic:
← UpperHalfPlane.petersson_slash_SL

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f ∣[k] g) (⇑f' ∣[k] g) τ) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun n z ↦ ∑ x ∈ n, eisSummand k (↑x) z) (⇑(eisensteinSeriesSIF a k)) Filter.atTop ⊤

Tactic:
simp only [Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]

Goal state after:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (fun n z ↦ ∑ x ∈ n, eisSummand k (↑x) z) (⇑(eisensteinSeriesSIF a k)) Filter.atTop
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ |↑g 1 0| ≤ 1

Tactic:
by
  let c' : ℤ := g 1 0
  let c := (c' : ℝ)
  suffices 3 * c ^ 2 ≤ 4 by
    rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_le] at this
    replace this : c' ^ 2 ≤ 1 ^ 2 := by lia
    rwa [sq_le_sq, abs_one] at this
  suffices c ≠ 0 → 9 * c ^ 4 ≤ 16 by
    rcases eq_or_ne c 0 with (hc | hc)
    · simp [hc]
    · apply le_of_sq_le_sq <;> grind
  intro hc
  have h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
    gcongr <;> exact three_le_four_mul_im_sq_of_mem_fd (by assumption)
  have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
    div_le_one_of_le₀
      (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g)) (sq_nonneg _)
  calc
    9 * c ^ 4 ≤ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
    _ = c ^ 4 * z.im ^ 4 / normSq (denom g z) ^ 2 * 16 := by grind [im_smul_eq_div_normSq]
    _ ≤ 16 := by rw [← mul_pow]; linarith

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: x : ↥(divisorsAntidiagonal 1)
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)

Tactic:
have h := Nat.mem_divisorsAntidiagonal.mp x.2
  simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h
  simp [divisorsAntidiagonalFactors, h.1, h.2]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
hSre : (S • z).re = -z.re
this : |↑(↑g 0 0) + (S • z).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
hSre

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
hSre : (S • z).re = -z.re
this : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
⊢ ↑((↑A * ↑B) 1 0) / denom (toGL (φ A) * toGL (φ B)) ↑z =
    ↑(↑A 1 0) / denom (toGL (φ A)) ↑(toGL (φ B) • z) * (denom (toGL (φ B)) ↑z ^ 2)⁻¹ + ↑(↑B 1 0) / denom (toGL (φ B)) ↑z

Tactic:
have : denom A (num B z / denom B z) = denom A ↑(B • z) := by
    simp [specialLinearGroup_apply, denom, num]

Goal state after:
A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) / denom (toGL (φ A) * toGL (φ B)) ↑z =
    ↑(↑A 1 0) / denom (toGL (φ A)) ↑(toGL (φ B) • z) * (denom (toGL (φ B)) ↑z ^ 2)⁻¹ + ↑(↑B 1 0) / denom (toGL (φ B)) ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl.inl
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 ^ 1 * S
hSre : (S • z).re = -z.re
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
zpow_one

Goal state after:
case inr.inr.inl.inl
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 * S
hSre : (S • z).re = -z.re
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ (fun m ↦ ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))⁻¹) =O[cofinite] fun n ↦ (‖n‖ ^ 3)⁻¹

Tactic:
simpa [pow_three, pow_two, ← mul_assoc] using ((isBigO_linear_add_const_vec z 0 1).mul
      (isBigO_linear_add_const_vec z 0 0)).mul (isBigO_linear_add_const_vec z 0 0)

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

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : (G2 ∣[2] g) ∣[2] g⁻¹ = (G2 - D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
← SlashAction.slash_mul,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 ∣[2] (g * g⁻¹) = (G2 - D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
⊢ ‖r‖ < 1

Tactic:
simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]

Goal state after:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
⊢ ∀ (x : ↑K), ‖cexp (2 * ↑π * I * ↑x / ↑p)‖ < 1
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • ⇑(E hk)) - qExpansion 1 ⇑f) = 0

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
ModularForm.qExpansion_smul,

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • qExpansion 1 ⇑(E hk) - qExpansion 1 ⇑f) = 0

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ 1 + ↑(if k - 12 ≡ 2 [MOD 12] then (k - 12) / 12 else (k - 12) / 12 + 1) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]

Goal state after:
case h.inr.inr
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ 1 + ↑(if k % 12 = 2 % 12 then (k - 12) / 12 else (k - 12) / 12 + 1) =
    ↑(if k % 12 = 2 % 12 then (k - 12) / 12 + 1 else (k - 12) / 12 + 1 + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.refine_1
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun x_1 ↦ ‖↑(↑ofComplex (↑x_1 * ↑x))‖) (𝓝 1) (𝓝 ‖↑x‖)

Tactic:
have : ContinuousAt (fun a : ℝ ↦ (ofComplex (a * x : ℂ) : ℂ)) 1 := by
        refine .comp (by fun_prop) ((OpenPartialHomeomorph.continuousAt _ ?_).comp (by fun_prop))
        simpa [ofComplex] using x.coe_im_pos

Goal state after:
case h.refine_1
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
this : ContinuousAt (fun a ↦ ↑(↑ofComplex (↑a * ↑x))) 1
⊢ Filter.Tendsto (fun x_1 ↦ ‖↑(↑ofComplex (↑x_1 * ↑x))‖) (𝓝 1) (𝓝 ‖↑x‖)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (E hk) z = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n

Tactic:
by
  convert! q_expansion_riemannZeta hk hk2 z using 1
  rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ |x.re| < 1 / 2

Tactic:
· rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]
    apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)
    rw [Set.image_subset_iff]
    intro ξ hξ
    simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 0)

Tactic:
show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (fun a ↦ ∑ c, (quotientFunc f c ∣[k] γ) a) atImInfty (𝓝 (∑ c, 0))
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
⊢ ModularForm.norm ℋ f = 0 ↔ ⇑f = 0

Tactic:
refine ⟨fun hn ↦ ?_, fun hf ↦ ?_⟩
  · contrapose! hn
    exact norm_ne_zero ℋ hn
  · ext τ
    simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk]
      using ⟨1, by simpa using congr_fun hf τ⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
c : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * (p * c)
⊢ n + 1 = p ^ (multiplicity p (n + 1) + 1) * c

Tactic:
rwa [pow_succ, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Fintype.card (InfinitePlace ↥K⁺) = Fintype.card (InfinitePlace K)

Tactic:
rw [card_eq_nrRealPlaces_add_nrComplexPlaces, card_eq_nrRealPlaces_add_nrComplexPlaces,
    IsTotallyComplex.nrRealPlaces_eq_zero K, IsTotallyReal.nrComplexPlaces_eq_zero, zero_add,
    add_zero, ← IsTotallyReal.finrank, ← Nat.mul_left_cancel_iff zero_lt_two,
    ← IsTotallyComplex.finrank, ← Module.finrank_mul_finrank ℚ K⁺ K, mul_comm,
    IsQuadraticExtension.finrank_eq_two _ K]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtAllPlaces (mixedSpaceOfRealSpace (normAtAllPlaces a)) ∈ normAtAllPlaces '' A

Tactic:
normAtAllPlaces_normAtAllPlaces

Goal state after:
case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ ↑((RingOfIntegers.mapRingEquiv (complexConj K).toRingEquiv) ↑u) = ↑↑u ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u

Tactic:
RingOfIntegers.mapRingEquiv_apply,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ (complexConj K).toRingEquiv ↑↑u = ↑↑u ↔ ∃ v, ↑((algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v) = ↑↑u