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

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

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

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

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

Tactic:
· rw [zero_sub, ← integral_neg]
    refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
    rw [deriv_ofReal_cpow_const (zero_lt_one.trans ht).ne', h₄]
    · ring_nf
    · exact neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)

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

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

case convert_3
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ (fun t ↦ deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k) =O[atTop] fun x ↦ x ^ ((-s - 1).re + r)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
⊢ J(a | 0) = 1

Tactic:
by
  simp only [jacobiSym, primeFactorsList_zero, List.prod_nil, List.pmap]

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

Goal state before:
pp: a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a ^ x✝ | b) * J(a | b) = J(a | b) ^ x✝ * J(a | b)

Tactic:
ih

Goal state after:
a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a | b) ^ x✝ * J(a | b) = J(a | b) ^ x✝ * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ e) * J(a | b) = J(a | b) ^ e * J(a | b)

Tactic:
ih

Goal state after:
case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b) ^ e * J(a | b) = J(a | b) ^ e * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n | n✝) * J(l'.prod | n✝) = J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod

Tactic:
ih

Goal state after:
case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod = J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * (a * x * y) = y * (a * (x * y))

Tactic:
rw [mul_assoc a x y]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
h : ↑(sMod p (p - 2)) = 0
⊢ ?m.28 ∣ sMod p (p - 2)

Tactic:
simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2

Tactic:
ih

Goal state after:
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2

Tactic:
rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']
    exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : ↑(s (p' + 2 - 2)) = 0
⊢ 2 ^ (p' + 2) - 1 ∣ s p'

Tactic:
simpa [ZMod.intCast_zmod_eq_zero_iff_dvd] using h

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : Nat.blt 1 p = true
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p

Tactic:
rw [Nat.blt_eq] at hp

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

Goal state before:
pp: p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p

Tactic:
rw [Nat.blt_eq] at hp

Goal state after:
p : ℕ
hp : 1 < p
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p
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✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
⊢ |↑(GeneralLinearGroup.det g)| = 1

Tactic:
rcases HasDetPlusMinusOne.det_eq hg with h | h

Goal state after:
case inl
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_2
inst✝³ : CommRing R
Γ : Subgroup (GL n R)
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = 1
⊢ |↑(GeneralLinearGroup.det g)| = 1

case inr
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
R : Type u_2
inst✝³ : CommRing R
Γ : Subgroup (GL n R)
inst✝² : LinearOrder R
inst✝¹ : IsOrderedRing R
inst✝ : Γ.HasDetPlusMinusOne
g : GL n R
hg : g ∈ Γ
h : GeneralLinearGroup.det g = -1
⊢ |↑(GeneralLinearGroup.det g)| = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Tactic:
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]

Goal state after:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢

Tactic:
rw [← isCusp_iff_of_relIndex_ne_zero inf_le_right hGH] at hc

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c (𝒢 ⊓ ℋ)
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ (ConjAct.toConjAct h • 𝒢).relIndex (ConjAct.toConjAct h • ℋ) ≠ 0

Tactic:
𝒢.relIndex_pointwise_smul

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
c : OnePoint ℚ
⊢ IsCusp (OnePoint.map Rat.cast c) (mapGL ℝ).range

Tactic:
obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ

Goal state after:
case mpr
a : SL(2, ℤ)
⊢ IsCusp (OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)) (mapGL ℝ).range
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map (⇑(Rat.castHom ℝ)) ((mapGL ℚ) a • ∞) =
    OnePoint.map (⇑(Rat.castHom ℝ)) ((mapGL ℚ) a • ∞)

Tactic:
← (Rat.castHom ℝ).algebraMap_toAlgebra

Goal state after:
case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞) =
    OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞)
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ 0 < ↑(Matrix.GeneralLinearGroup.det (J * g))

Tactic:
simpa using hg

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

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝

Tactic:
exact DFunLike.ext' h

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

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝

Tactic:
exact DFunLike.ext' h

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * (starRingEnd ℂ) (f c)).im = c 1

Tactic:
rw [f_def, map_add, map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal,
        conj_ofReal, ← ofReal_mul, add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]

Goal state after:
case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z * ↑(c 1)).im = (↑z).im * c 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_3
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := ⋯
hmB : Continuous mB
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := ⋯
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
⊢ (mB ∘ fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) = ⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a

Tactic:
ext ⟨g, rfl⟩ i j : 3

Goal state after:
case e'_3
f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g ↦ (↑g).map Int.cast
cocompact_ℝ_to_cofinite_ℤ_matrix : Tendsto (fun m ↦ m.map Int.cast) cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
hf₁ : Tendsto f₁ cofinite (cocompact (Matrix (Fin 2) (Fin 2) ℝ))
g : SL(2, ℤ)
hcd : IsCoprime (↑g 1 0) (↑g 1 1)
mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t ↦ of ![![t, -↑1], Int.cast ∘ ↑g 1]
hmB : Continuous mB
hf₂ : IsClosedEmbedding ⇑(lcRow0Extend hcd)
i j : Fin 2
⊢ (mB ∘ fun g_1 ↦ (lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g_1)) ⟨g, ⋯⟩ i j =
    (⇑(lcRow0Extend hcd) ∘ f₁ ∘ fun a ↦ ↑a) ⟨g, ⋯⟩ i j
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
⊢ ∞.IsZeroAt (⇑f ∣[k] (g * γ)) ?m.65

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
⊢ ℤ

Tactic:
← OnePoint.IsZeroAt.smul_iff

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
⊢ ((g * γ) • ∞).IsZeroAt (⇑f) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ ∞.IsZeroAt (⇑f ∣[k] toGL ((map (Int.castRingHom ℝ)) g)) ?m.27

pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ ℤ

Tactic:
← OnePoint.IsZeroAt.smul_iff

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ (toGL ((map (Int.castRingHom ℝ)) g) • ∞).IsZeroAt (⇑f) k
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
⊢ Tendsto (fun g ↦ (↑g • z).re) cofinite (cocompact ℝ)

Tactic:
let ff := Homeomorph.addRight
    (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re

Goal state after:
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
this : (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ ≠ 0
f : ℝ ≃ₜ ℝ := Homeomorph.mulRight₀ (↑(p 0) ^ 2 + ↑(p 1) ^ 2)⁻¹ this
ff : ℝ ≃ₜ ℝ := Homeomorph.addRight ((↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))).re
⊢ Tendsto (fun g ↦ (↑g • z).re) cofinite (cocompact ℝ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case pos
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : r = 0
⊢ v = r • divIntMap (↑r) v

Tactic:
have hv := hv.2

Goal state after:
case pos
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 r 0
hr : r = 0
hv : (v 0).gcd (v 1) = r
⊢ v = r • divIntMap (↑r) v
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : ↑z * c + d ≠ 0
⊢ ((u * (a * ↑z + b) + (↑z * c + d) * v) / (↑z * c + d)) ^ (-k) =
    (↑z * c + d) ^ k * (↑z * (u * a + c * v) + (u * b + d * v)) ^ (-k)

Tactic:
simp [div_zpow]

Goal state after:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : ↑z * c + d ≠ 0
⊢ (↑z * c + d) ^ k / (u * (a * ↑z + b) + (↑z * c + d) * v) ^ k =
    (↑z * c + d) ^ k * ((↑z * (u * a + c * v) + (u * b + d * v)) ^ k)⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : ↑3 * ↑(c' ^ 2) ≤ 4
⊢ |↑g 1 0| ≤ 1

Tactic:
← Int.cast_four,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : ↑3 * ↑(c' ^ 2) ≤ ↑4
⊢ |↑g 1 0| ≤ 1
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
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ

Tactic:
have hgeq : g = T ^ g 0 0 * S * T := by
    refine Subtype.ext ?_
    rw [coe_mul, coe_mul, coe_T_zpow, coe_S, coe_T, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]
    grind [g.property, det_fin_two]
  rw [hgeq]
  obtain ⟨hnorm, hre⟩ : normSq z = 1 ∧ z.re = -1 / 2 := by
    have hnorm : normSq ((z : ℂ) + 1) ≤ 1 := by simpa [denom, hc, hd, norm_def] using hg'
    have : normSq (z + 1) = normSq z + (2 * z.re + 1) := by simp [normSq]; ring
    rw [this] at hnorm
    constructor <;> linarith [hz.1, show 0 ≤ 2 * z.re + 1 by linarith [(neg_le_abs _).trans hz.2]]
  have hρ : z = ρ := by
    apply eq_of_re_of_norm
    · simp [hre, ρ]
    · rw [norm_def, hnorm, norm_ρ, Real.sqrt_one]
  refine ⟨?_, hρ⟩
  have hSTρ : (S * T) • ρ = ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, eq_comm, UpperHalfPlane.ext_iff,
      modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk, coe_vadd,
      ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
    grind [ρ_sq, ofReal_one]
  rw [hgeq, hρ, mul_assoc, mul_smul, hSTρ] at hg
  suffices g 0 0 = 0 ∨ g 0 0 = 1 by rcases this with h | h <;> simp [h]
  have hgzre := hg.2
  simp only [Fin.isValue, ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re,
    abs_le, le_add_iff_nonneg_right, Int.cast_nonneg_iff, neg_add_le_iff_le_add,
    show (2⁻¹ : ℝ) + 2⁻¹ = 1 by norm_num] at hgzre
  rw [← Int.cast_one (R := ℝ), Int.cast_le] at hgzre
  grind

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
⊢ ↑g 0 1 = -↑g 0 0 - 1

Tactic:
have := g.property

Goal state after:
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).det = 1
⊢ ↑g 0 1 = -↑g 0 0 - 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ G2 ∣[2] h + (-D2 g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)

Tactic:
ih

Goal state after:
case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ G2 - D2 h + (-D2 g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)
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
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (deriv (F ∘ ↑ofComplex) ↑z - deriv (G ∘ ↑ofComplex) ↑z) =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z

Tactic:
mul_sub

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z - (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z
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
⊢ -g • z ∈ 𝒟

Tactic:
simpa using hg

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

Goal state before:
pp: c✝ : OnePoint ℝ
hc : IsCusp c✝ (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • OnePoint.infty = c✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [slash_action_generators_SL2Z discriminant_S_invariant discriminant_T_invariant]

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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        (g • z).im = z.im →
          0 ≤ ↑g 1 0 →
            (g = 1 ∨ g = -1) ∨
              (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
                (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
                  (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
                    (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
                      (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                        (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                          (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                            (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ ↑g 1 0
⊢ -g • z ∈ 𝒟

Tactic:
simpa using hg

Goal state after: