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

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
by_cases hψ₀ : ψ = 1

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx✝ hx : eval₂ i x f = 0
z w : S
⊢ eval₂ i x (h.repr (z + w)) = eval₂ i x (h.repr z) + eval₂ i x (h.repr w)

Tactic:
simp [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w)]

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

Goal state before:
pp: q : ℚ
hq₀ : ↑q.den ≠ 0
⊢ mulHeight ![q, 1] = mulHeight ![↑q.num, ↑q.den]

Tactic:
rw [← mulHeight_smul_eq_mulHeight _ hq₀]

Goal state after:
q : ℚ
hq₀ : ↑q.den ≠ 0
⊢ mulHeight (↑q.den • ![q, 1]) = mulHeight ![↑q.num, ↑q.den]
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ (algebraMap ℚ ℝ) (Polynomial.eval 1 (Polynomial.bernoulli k)) = ↑(bernoulli k)

Tactic:
Polynomial.bernoulli_eval_one,

Goal state after:
k : ℕ
hk : k ≠ 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case inl.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Tactic:
· rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]

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

Goal state before:
pp: case e_a.e_f.inr.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

pp: case e_a.e_f.inr.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hΦ' : Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
· rw [hurwitzZetaEven_def_of_ne_or_ne (.inr hs)]

Goal state after:
case e_a.e_f.inr.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hΦ' : Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
⊢ ‖↑a * z‖ < 1

Tactic:
rwa [norm_mul, hz, mul_one]

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

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 0 < (↑↑p)⁻¹

Tactic:
by have := p.prop.pos; positivity

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

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

pp: case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
· refine (continuousOn_neg_logDeriv_LFunctionTrivChar₁ q).mono fun s hs ↦ ?_
    simp only [ne_eq, Set.mem_ofPred_eq] at hs
    tauto

Goal state after:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ -∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
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

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp ↦ legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ legendreSym p 1 = 1

Tactic:
legendreSym.at_one

Goal state after:
b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp ↦ legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ 1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ ((-1) ^ (a / 2)) ^ (b / 2) * J(↑b | a) = J(↑b | a)

Tactic:
neg_one_pow_div_two_of_one_mod_four ha,

Goal state after:
a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ 1 ^ (b / 2) * J(↑b | a) = J(↑b | a)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Tactic:
simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, Set.mem_univ,
      IsLocalRing.residue, Set.mem_image, true_implies]

Goal state after:
case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ ∃ x_1 ∈ t,
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K])) x_1 = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥𝒪[K])) x
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
⊢ IsTopologicalDivisionRing K

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
this : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
⊢ IsTopologicalDivisionRing K
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
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:
let := IsTopologicalAddGroup.rightUniformSpace K

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
⊢ Nonempty (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))

Tactic:
let := IsTopologicalAddGroup.rightUniformSpace K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
this : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
⊢ Nonempty (ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : 2 ^ (p' + 2) - 1 ∣ s p'
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
obtain ⟨k, h⟩ := h

Goal state after:
p' : ℕ
k : ℤ
h : s p' = (2 ^ (p' + 2) - 1) * k
⊢ ∃ k, ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
p' : ℕ
hp' : p' = p - 2
⊢ LucasLehmerTest p → Nat.Prime (mersenne p)

Tactic:
obtain rfl : p = p' + 2 := by lia

Goal state after:
p' : ℕ
w : 1 < p' + 2
hp' : p' = p' + 2 - 2
⊢ LucasLehmerTest (p' + 2) → Nat.Prime (mersenne (p' + 2))
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
⊢ LucasLehmerTest p

Tactic:
obtain rfl : p = p' + 2 := by lia

Goal state after:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ LucasLehmerTest (p' + 2)
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)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * (↑a₂ * (↑M * ↑a₁)) * (↑A₁.den)⁻¹) • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
inv_mul_cancel_left₀ (mod_cast A₂.den_ne_zero),

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)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    (↑M * ↑a₁ * (↑A₁.den)⁻¹) • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
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
⊢ ⟨z, hz_det⟩ ∈ ↑Γ(M)

Tactic:
rw [SetLike.mem_coe, CongruenceSubgroup.Gamma_mem', Subtype.ext_iff]

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
⊢ ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M))) ⟨z, hz_det⟩) = ↑1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.map (mapGL ℝ) ⊤).relIndex
      (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0

Tactic:
← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹,

Goal state after:
case right
g : GL (Fin 2) ℚ
⊢ ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤).relIndex
      ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ •
        toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ OnePoint.map (⇑(Rat.castHom ℝ)) ((mapGL ℚ) g • ∞) = (mapGL ℝ) g • ∞

Tactic:
OnePoint.map_smul,

Goal state after:
case mp
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g • ∞

Tactic:
OnePoint.map_infty,

Goal state after:
case mp
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ OnePoint.map (⇑(Rat.castHom ℝ)) ((mapGL ℚ) g • ∞) = (mapGL ℝ) g • ∞

Tactic:
OnePoint.map_smul,

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g • ∞

Tactic:
OnePoint.map_infty,

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g) • ∞ = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ OnePoint.map (⇑(Rat.castHom ℝ)) ((mapGL ℚ) g⁻¹ • ∞) = (mapGL ℝ) g⁻¹ • ∞

Tactic:
OnePoint.map_smul,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g⁻¹) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g⁻¹ • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g⁻¹) • OnePoint.map ⇑(Rat.castHom ℝ) ∞ = (mapGL ℝ) g⁻¹ • ∞

Tactic:
OnePoint.map_infty,

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ (GeneralLinearGroup.map (Rat.castHom ℝ)) ((mapGL ℚ) g⁻¹) • ∞ = (mapGL ℝ) g⁻¹ • ∞
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
⊢ 1 ≤ (qExpansionFormalMultilinearSeries h f).radius

Tactic:
by
  refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_
  lift r to NNReal using hr.ne_top
  apply FormalMultilinearSeries.le_radius_of_summable
  simp only [qExpansionFormalMultilinearSeries_apply_norm]
  rw [← r.abs_eq]
  simp_rw [← Real.norm_eq_abs, ← Complex.norm_real, ← norm_pow, ← norm_mul]
  exact (UpperHalfPlane.hasSum_qExpansion_of_norm_lt hh hfper hfhol hfbdd
    (by simpa using hr)).summable.norm

Goal state after:
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:
have hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / (im τ) ^ t) (truncatedFundamentalDomain y) := by
    apply (hf_cont.norm.div ?_ fun τ ↦ by positivity).continuousOn
    exact continuous_im.rpow_const fun τ ↦ .inl τ.im_ne_zero

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
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case pos
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 : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this✝ : ↑g 1 1 ≠ 0
this : 1 ≤ ↑(↑g 1 1) ^ 2
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ τ.im

Tactic:
rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]

Goal state after:
case pos
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 : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this✝ : ↑g 1 1 ≠ 0
this : 1 ≤ ↑(↑g 1 1) ^ 2
⊢ τ.im / ↑(↑g 1 1) ^ 2 ≤ τ.im
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case refine_3
r : ℕ
inst✝ : NeZero r
⊢ SurjOn (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)

Tactic:
· intro x hx
    use r • x
    simp only [nsmul_eq_mul, divIntMap, Int.cast_natCast]
    constructor
    · rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
      exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩
    · ext i
      simp_all [NeZero.ne r]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
⊢ 1 < normSq ↑(T ^ n • z)

Tactic:
by
  rw [coe_T_zpow_smul_eq]
  have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1
  have hzn := Int.nneg_mul_add_sq_of_abs_le_one n (abs_two_mul_re_lt_one_of_mem_fdo hz).le
  have : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im := by linarith
  simpa [normSq, num, denom]

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

Goal state before:
pp: h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1

Tactic:
have h2 : iteratedDeriv m (1 : ℂ → ℂ) 0 = if m = 0 then 1 else 0 := by
    simpa [ite_apply] using! iteratedDeriv_const

Goal state after:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
h2 : iteratedDeriv m 1 0 = if m = 0 then 1 else 0
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1
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
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ e

Tactic:
have hh : 0 < h := Γ.strictWidthInfty_pos_iff.mpr Fact.out

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
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ e
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
⊢ 𝕢 1 z ∈ Metric.ball 0 1

Tactic:
simpa using norm_qParam_lt_one 1 ⟨z, hz⟩

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

Goal state before:
pp: case hf
z : ℍ
⊢ Tendsto (fun N ↦ ∑ n ∈ Finset.Ico (-↑N) ↑N, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))

Tactic:
apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)

Goal state after:
z : ℍ
x : ℕ
⊢ ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑x) ↑x, 1 / (↑n * ↑z + ↑m) ^ 2 =
    ∑ n ∈ Finset.Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem
γ g : SL(2, ℤ)
hg : g = S ∨ g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
rcases hg with (h1 | h2)

Goal state after:
case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
⊢ G2 ∣[2] g = G2 - D2 g

case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ z.im ≤ (-g • z).im

Tactic:
by simpa using hden

Goal state after:
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)
⊢ 2 * I * (E2 z * ↑π - 6 * I * ↑1 / ↑z) = 12 / ↑z + E2 z * ↑π * 2 * I

Tactic:
grind [I_sq]

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

Goal state before:
pp: case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet

Tactic:
apply DifferentiableOn.comp (t := upperHalfPlaneSet)
    · exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt
    · exact DifferentiableOn.div (by fun_prop) (by fun_prop)
        (fun x hx ↦ ne_zero (⟨x, hx⟩ : ℍ))
    · exact fun y hy ↦ by grind [im_pnat_div_pos 1 (⟨y, hy⟩ : ℍ)]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

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

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

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑ n ∈ Ico (-↑N) ↑N, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) atTop (𝓝 ((↑z ^ 2)⁻¹ * G2 (S • z)))

Tactic:
apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)

Goal state after:
z : ℍ
x : ℕ
⊢ ∑' (n : ℤ), ∑ m ∈ Ico (-↑x) ↑x, 1 / (↑n * ↑z + ↑m) ^ 2 = ∑ n ∈ Ico (-↑x) ↑x, ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2