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

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

Tactic:
by_cases h' : ∑ j, Φ j = 0

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
h' : ∑ j, Φ j = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ

case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
x : ℂ
h : ¬Φ 0 = 0
h' : ¬∑ j, Φ j = 0
⊢ x ∈ U ↔ x ∈ Ucᶜ
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
ofReal_pow

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑↑n ^ (2 * k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))

Tactic:
convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)) = fun n ↦
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * (fourier (-↑n)) ↑x)

case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) =
    -(2 * ↑π * I) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1.refine_2
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun x ↦ x + 1
u : Nat.Primes × ℕ
hu : u.2 = 0
⊢ F' u = 0

Tactic:
rw [← hF'₀ u.1, ← hu]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
ofReal_pow

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = 1 / ↑↑x✝ ^ (2 * k + 1)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ LSeriesSummable f s

Tactic:
LSeriesSummable,

Goal state after:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ Summable (LSeries.term f s)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ}, x ∈ Set.Icc 1 2 → C ≤ (LFunctionResidueClassAux a ↑x).re
x : ℝ
hx : x ∈ Set.Ioc 1 2
⊢ (↑q.totient)⁻¹ / (x - 1) - -C ≤ (↑q.totient)⁻¹ / (x - 1) + (LFunctionResidueClassAux a ↑x).re

Tactic:
sub_neg_eq_add,

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ}, x ∈ Set.Icc 1 2 → C ≤ (LFunctionResidueClassAux a ↑x).re
x : ℝ
hx : x ∈ Set.Ioc 1 2
⊢ (↑q.totient)⁻¹ / (x - 1) + C ≤ (↑q.totient)⁻¹ / (x - 1) + (LFunctionResidueClassAux a ↑x).re
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
by aesop

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

Goal state before:
pp: a b c : ℕ
hb0 : 0 < b
hc : a / b ≤ c
x : ℕ
h : x * b ≤ a
⊢ x ≤ a / b

Tactic:
by rwa [le_div_iff_mul_le hb0]

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : IsNontrivial R
hM : MulArchimedean (ValueGroupWithZero R)
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
rw [isNontrivial_iff_nontrivial_units] at hN

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
⊢ IsDiscrete R

Tactic:
have : IsRankLeOne R := .of_compatible_mulArchimedean v
  by_cases h : IsNontrivial R
  · by_cases H : DenselyOrdered (ValueGroupWithZero R)
    · classical
      exfalso
      refine (MonoidWithZeroHom.range_nontrivial
        (ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).not_subsingleton ?_
      rw [← WithZero.denselyOrdered_set_iff_subsingleton]
      exact (ValueGroupWithZero.embed_strictMono v).denselyOrdered_range
    · rw [isNontrivial_iff_nontrivial_units] at h
      rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H
      rw [nonempty_orderIso_withZeroMul_int_iff] at H
      exact H.left
  · rw [isNontrivial_iff_nontrivial_units] at h; push Not at h
    refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
    contrapose! hy
    have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
    exact Units.val_le_val.mpr this.le

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

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ J(a | b) = (List.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod

Tactic:
rw [jacobiSym, List.map_map, ← List.pmap_eq_map
    fun _ => prime_of_mem_primeFactorsList]

Goal state after:
a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | b) = 1

Tactic:
hb1,

Goal state after:
case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : b = 1
⊢ J(a | 1) = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ Topology.IsEmbedding ⇑(map (Int.castRingHom ℝ))

Tactic:
exact Real.isClosedEmbedding_intCast.specialLinearGroup_map.1

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ (1 + (M • (A₁.num * k * A₂.num)).map fun x ↦ ↑x) i j = ↑1 i j

Tactic:
Matrix.add_apply,

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ 1 i j + (M • (A₁.num * k * A₂.num)).map (fun x ↦ ↑x) i j = ↑1 i j
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case refine_2
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p) • g • c = g • c

Tactic:
simp [ConjAct.toConjAct_smul, mul_smul, hpc]

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsZeroAtImInfty (f ∣[k] g) → c.IsZeroAt f k

Tactic:
by simp [← hg, IsZeroAt.smul_iff, isZeroAt_infty_iff]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ ↑ofComplex) q = (f ∘ ↑ofComplex) (Periodic.invQParam h q)
⊢ HasSum (fun m ↦ c m • q ^ m) (cuspFunction h f q)

Tactic:
have : cuspFunction h f q = f τ := by simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1]
    using! h2

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
h1 : 0 < (Periodic.invQParam h q).im
τ : ℍ := { coe := Periodic.invQParam h q, coe_im_pos := h1 }
h2 : Periodic.cuspFunction h (f ∘ ↑ofComplex) q = (f ∘ ↑ofComplex) (Periodic.invQParam h q)
this : cuspFunction h f q = f τ
⊢ HasSum (fun m ↦ c m • q ^ m) (cuspFunction h f q)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (↑z).im = z.im

Tactic:
coe_im

Goal state after:
z : ℍ
n : ℤ
⊢ z.im = z.im
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s ↦ (fun z ↦ ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    (⇑(eisensteinSeriesSIF a k) ∘ ↑ofComplex) Filter.atTop {z | 0 < z.im}

Tactic:
rw [← upperHalfPlaneSet, ← range_coe, ← image_univ]

Goal state after:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s ↦ (fun z ↦ ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    (⇑(eisensteinSeriesSIF a k) ∘ ↑ofComplex) Filter.atTop (UpperHalfPlane.coe '' Set.univ)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
hg' : AnalyticAt ℂ (cuspFunction h (-g)) 0
⊢ qExpansion h (f - g) = qExpansion h f - qExpansion h g

Tactic:
simpa [sub_eq_add_neg, qExpansion_neg hg] using (qExpansion_add hf hg')

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

Goal state before:
pp: case h
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ ∀ x ∈ {z | 0 < z.im}, ↑(a 0) * x + ↑(a 1) ≠ 0

Tactic:
exact fun z hz ↦ linear_ne_zero ⟨z, hz⟩
        ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)

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:
refine hC.trans (congrArg (C * ·) ?_).le

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‖
⊢ max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖ = max 1 (1 / τ.im ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1
⊢ Tendsto (fun m ↦ ∑' (n : ℕ+), r ^ (↑n * ↑m)) atTop (𝓝 0)

Tactic:
rw [funext h2, (by simp : 𝓝 (0 : 𝕜) = 𝓝 ((1 - 0)⁻¹ - 1)), tendsto_sub_const_iff,
    tendsto_inv_iff₀ (by simp), tendsto_const_sub_iff]

Goal state after:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
h2 : ∀ (m : ℕ+), ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1
⊢ Tendsto (fun x ↦ r ^ ↑x) atTop (𝓝 0)
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
⊢ (-↑z).re / ‖↑z‖ ^ 2 = -z.re

Tactic:
hz',

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
⊢ (-↑z).re / 1 ^ 2 = -z.re
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: s : Set (Finset ℤ)
⊢ (∃ a, ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s) ↔ ∃ a, ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
  [convert! ha (b - 1) (by grind) using 1; convert! ha (b + 1) (by grind) using 1] <;>
  simp [Finset.ext_iff]

Goal state after:
s : Set (Finset ℤ)
x✝ : ∃ a, ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-↑b) ↑b ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ ∀ (a : ℤ), -↑b < a ∧ a < ↑b ↔ -↑(b - 1) ≤ a ∧ a ≤ ↑(b - 1)

s : Set (Finset ℤ)
x✝ : ∃ a, ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-↑b) ↑b ∈ s
b : ℕ
hb : a - 1 ≤ b
⊢ ∀ (a : ℤ), -↑b ≤ a ∧ a ≤ ↑b ↔ -1 < a + ↑b ∧ a < ↑b + 1
Module: Mathlib.NumberTheory.Modular

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

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

Tactic:
· have := this.trans_lt ((add_lt_add_iff_left _).mpr hzre)
    rw [add_halves, ← Int.cast_abs, ← Int.cast_one (R := ℝ), Int.cast_lt] at this
    grind [Int.abs_lt_one_iff, zpow_zero]

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

Tactic:
hz',

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

Goal state before:
pp: z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ![↑b, ↑n + 1] ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
h0 : ↑b * ↑z + ↑n + 1 ≠ 0
⊢ ![↑b, ↑n] ≠ 0

Tactic:
by aesop

Goal state after:
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 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
⊢ ↑z - 1 = denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z

Tactic:
simp [denom, hc, hd, sub_eq_add_neg]

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 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) - -D2 g⁻¹ - D2 g⁻¹

Tactic:
sub_neg_eq_add,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) + D2 g⁻¹ - D2 g⁻¹
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + logDeriv η ↑z

Tactic:
logDeriv_eta_eq_E2 z,

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (↑z ^ 2)⁻¹ * logDeriv η (-↑z)⁻¹ = ↑z ^ (-1 / 2) / 2 * (↑z).sqrt⁻¹ + ↑π * I / 12 * E2 z
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‖
x : ↑K
h1 : cexp (2 * ↑π * I * (↑x / ↑p)) = cexp (2 * ↑π * I * ↑x / ↑p)
⊢ 0 < (↑x / ↑p).im

Tactic:
by aesop

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

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ![↑m, ↑a] ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ![↑m, ↑b] ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ -↑↑d ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
rw [← closure_closure]

Goal state after:
x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure (closure 𝒟ᵒ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.h₁
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ |z.re| ≤ 1 / 2

Tactic:
exact hz.2.2.1

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

Goal state before:
pp: ⊢ (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (modularForm CuspForm.discriminant) =
    (1 / 1728) •
      ((DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) E₄ ^ 3 -
        (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) E₆ ^ 2)

Tactic:
by
  simp only [ModularForm.directSum_of_pow]
  change DirectSum.of (ModularForm 𝒮ℒ) 12 CuspForm.discriminant = (1 / 1728 : ℂ) •
    (DirectSum.of (ModularForm 𝒮ℒ) 12 (E₄.pow 3) - DirectSum.of (ModularForm 𝒮ℒ) 12 (E₆.pow 2))
  rw [← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12), ← DirectSum.of_smul]
  congr 1
  ext z
  change ModularForm.discriminant z = (1 / 1728 : ℂ) * (E₄ z ^ 3 - E₆ z ^ 2)
  grind [discriminant_eq_E₄_cube_sub_E₆_sq z]

Goal state after: