mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
let g : R →ₗ[R] (I ^ n : Ideal R) := (LinearMap.mulRight R ϖ ^ n).codRestrict _ fun x ↦ by
    simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply]
    -- TODO: change argument of Ideal.pow_mem_of_mem
    exact Ideal.mul_mem_left _ _ hϖ

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * ϖ * y
⊢ x ∈ I

Tactic:
mul_assoc,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ x ∈ I
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
| χ ↑b

Tactic:
rw [← prod_primeFactorsList hb.pos.ne', cast_list_prod, map_list_prod χ]

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.map (⇑χ) (List.map Nat.cast b.primeFactorsList)).prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
rw [quadratic_reciprocity (odd_iff.mpr (odd_of_mod_four_eq_one ha)) hb, pow_mul,
    neg_one_pow_div_two_of_one_mod_four ha, one_pow, one_mul]

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

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * ↑t ^ (-↑s - 1) - l * ↑t ^ (-↑s) = S t * ↑t ^ (-↑s - 1) - l * ↑t * ↑t ^ (-↑s - 1)

Tactic:
cpow_sub _ _ ht,

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t ^ 1) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t ^ 1) - l * ↑t * (↑t ^ (-↑s) / ↑t ^ 1)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t) - l * ↑t * (↑t ^ (-↑s) / ↑t)

Tactic:
mul_assoc,

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t) - l * (↑t * (↑t ^ (-↑s) / ↑t))
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
a c : A
⊢ a * (fun x_1 ↦ x * x_1) c ∈ Set.range fun x_1 ↦ x * x_1

Tactic:
exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥⊤

Tactic:
rw [← Subring.center_eq_top A]

Goal state after:
A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥(Subring.center A)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sZMod p i = ↑(sMod p i)

Tactic:
induction i <;> push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *] <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 4) * ω ^ ((q + 1) / 4) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0

Tactic:
mul_assoc,

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 4) * (ω ^ ((q + 1) / 4) * ωb ^ ((q + 1) / 4)) = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
A : ↥(Gamma0 N)
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A).det = 1

Tactic:
simp only [A.1.property, Int.cast_one]

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

Goal state before:
pp: case left
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (Γ ⊓ Γ').relIndex (mapGL ℝ).range ≠ 0

Tactic:
apply relIndex_inf_ne_zero <;> exact IsArithmetic.is_commensurable.1

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

Goal state before:
pp: case coe
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
q : K
⊢ ∃ g, (mapGL K) g • ∞ = ↑q

Tactic:
obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0
    exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩

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

Goal state before:
pp: case mpr
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N) →
    ∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x

Tactic:
· simp only [AddSubgroup.mem_map, AddSubgroup.mem_zmultiples_iff, existsAndEq, true_and,
      Units.ext_iff, mapGL_coe_matrix, map_apply_coe, forall_exists_index]
    refine fun a ha ↦ ⟨ModularGroup.T ^ (a * N), by simp [ModularGroup.coe_T_zpow], ?_⟩
    ext i j
    fin_cases i <;> fin_cases j <;> simp [ModularGroup.coe_T_zpow, ← ha]

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

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * ‖f x‖ * ‖↑x.im‖ ^ k) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
mul_assoc,

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * ‖↑x.im‖ ^ k)) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    2 * ↑π * Complex.I * (↑n.factorial)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  ∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z =
    2 * ↑π * Complex.I * ((↑n.factorial)⁻¹ * iteratedDeriv n (cuspFunction h f) 0)
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) (𝕢 1 ↑ξ)‖

Tactic:
simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
            one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : normSq ↑z < 1
⊢ z.im < (S • z).im

Tactic:
ModularGroup.im_smul_eq_div_normSq

Goal state after:
z : ℍ
h : normSq ↑z < 1
⊢ z.im < z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
enter [1, C, τ, 1]

Goal state after:
k : ℤ
hk : 0 ≤ 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✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖
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
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
enter [1, C, τ, 1]

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
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
⊢ qExpansion h ⇑f = 0 ↔ f = 0

Tactic:
have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
this : Fact (IsCusp OnePoint.infty Γ)
⊢ qExpansion h ⇑f = 0 ↔ f = 0
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: ⊢ Function.LeftInverse (fun x ↦ ⟨⟨↑x.1 * ↑x.2, ⋯⟩, ⟨(↑x.1, ↑x.2), ⋯⟩⟩) fun x ↦ divisorsAntidiagonalFactors x.fst x.snd

Tactic:
by
    rintro ⟨n, ⟨k, l⟩, h⟩
    rw [Nat.mem_divisorsAntidiagonal] at h
    ext <;> simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]

Goal state after:
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
this : ↑|↑g 0 0| < 1
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
← Int.cast_one (R := ℝ),

Goal state after:
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
this : ↑|↑g 0 0| < ↑1
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
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
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
← Int.cast_one (R := ℝ),

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
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 * T) • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T

Tactic:
mul_assoc,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : (T ^ ↑g 0 0 * (S * T)) • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ ↑g 0 0 ∧ ↑(↑g 0 0) ≤ 1
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = 1

Tactic:
← Int.cast_one (R := ℝ),

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
hSTρ : (S * T) • ρ = ρ
hgzre : 0 ≤ ↑g 0 0 ∧ ↑(↑g 0 0) ≤ ↑1
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : (T ^ ↑g 0 0 * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
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⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹

Tactic:
mul_assoc,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : (T ^ ↑g 0 0 * (S * T⁻¹)) • (1 +ᵥ ρ) ∈ 𝒟
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⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
⊢ g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
⊢ (g • z).im = z.im

pp: case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (g • z).im = z.im

Tactic:
· rcases cases_c_zero hz hg hc with h | h | h | h <;>
    rcases h with ⟨(rfl | rfl), -⟩ <;>
    simp only [← zpow_neg_one, im_T_zpow_smul, im_T_smul, one_smul, SL_neg_smul]

Goal state after:
case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hs2
⊢ IsOpen upperHalfPlaneSet

Tactic:
exact isOpen_upperHalfPlaneSet

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

Goal state before:
pp: p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : (PowerSeries.coeff 0) p4 = 1
hp6_0 : (PowerSeries.coeff 0) p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
⊢ p = 0

Tactic:
simp_all only [PowerSeries.coeff_zero_eq_constantCoeff]
  let D := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
  have hD0 : D.coeff 0 = c4 ^ 3 - c6 ^ 2 := by simp [D, hp4_0, hp6_0]
  have hD1 : D.coeff 1 = 720 * c4 ^ 3 + 1008 * c6 ^ 2 := by
    simp [D, pow_succ, PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ]
    grind
  grind [pow_eq_zero_iff, zero_smul]

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

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

Tactic:
exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0

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

Goal state before:
pp: case e_a.e_a
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
⊢ ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) =
    ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (↑(↑m * ↑n) * (2 * ↑π * I * ↑z))

Tactic:
exact tsum_congr₂ (fun m n ↦ by push_cast; ring_nf)

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

Goal state before:
pp: z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
      -(2 / ↑↑N) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑N) + 1 / (-↑↑m * ↑z + -↑↑N) - 1 / (↑↑m * ↑z + ↑↑N) - 1 / (-↑↑m * ↑z + ↑↑N))
⊢ Tendsto (fun N ↦ ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) atTop
    (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
rw [funext this, show -2 * π * I / z = 0 + -2 * π * I / z by ring]

Goal state after:
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
      -(2 / ↑↑N) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑N) + 1 / (-↑↑m * ↑z + -↑↑N) - 1 / (↑↑m * ↑z + ↑↑N) - 1 / (-↑↑m * ↑z + ↑↑N))
⊢ Tendsto
    (fun x ↦
      -(2 / ↑↑x) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑x) + 1 / (-↑↑m * ↑z + -↑↑x) - 1 / (↑↑m * ↑z + ↑↑x) - 1 / (-↑↑m * ↑z + ↑↑x)))
    atTop (𝓝 (0 + -2 * ↑π * I / ↑z))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, ↑ofComplex (↑x_1 * ↑x) ∈ 𝒟ᵒ

Tactic:
simp only [fdo, Set.mem_ofPred, Filter.eventually_and, one_lt_normSq_iff]

Goal state after:
case h
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ (∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, 1 < ‖↑(↑ofComplex (↑x_1 * ↑x))‖) ∧
    ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |(↑ofComplex (↑x_1 * ↑x)).re| < 1 / 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
⊢ ‖jacobiTheta τ - 1‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖

Tactic:
by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]

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

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
h1728 : 1728 * discriminant z = E₄ z ^ 3 - E₆ z ^ 2
⊢ discriminant z = (E₄ z ^ 3 - E₆ z ^ 2) / 1728

Tactic:
linear_combination h1728 / 1728

Goal state after: