mathlib-initiative/mathlib-tactics huggingface dataset:
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.map Int.cast = 1
i j : Fin 2
⊢ ↑0 = 0

Tactic:
by simp

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.map Int.cast = 1
i j : Fin 2
⊢ ↑1 = 1

Tactic:
by simp

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.map Int.cast - Matrix.map 1 Int.cast = 0
i j : Fin 2
⊢ ∀ (a₁_1 a₂_1 : ℤ), ↑(a₁_1 - a₂_1) = ↑a₁_1 - ↑a₂_1

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : OnePoint K
⊢ ![1, 0] ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : OnePoint K
t : K
⊢ ![t, 1] ≠ 0

Tactic:
by simp

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)
⊢ ∀ (a : ℤ), ↑((a₁ * a₂ * M) • a) = (a₁ * a₂ * M) • ↑a

Tactic:
by simp

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)
⊢ ∀ (a : ℤ), ↑(M • a) = M • ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
⊢ ![1, 0] ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
t : K
⊢ ![t, 1] ≠ 0

Tactic:
by simp

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

Goal state before:
pp: A : SL(2, ℤ)
x : ℂ
⊢ Function.const ℍ x ∣[0] A = Function.const ℍ x

Tactic:
by
  funext
  simp [SL_slash, slash_def, σ, zero_lt_one]

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

Goal state before:
pp: 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
⊢ (mapGL K) 1 • ∞ = ∞

Tactic:
by simp

Goal state after:
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:
rw [← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹,
      inv_smul_smul, ← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ 1 • ∞ = ∞

Tactic:
by simp

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ 1 • ∞ = ∞

Tactic:
by simp

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

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

Tactic:
by simp [← hg, IsBoundedAt.smul_iff, isBoundedAt_infty_iff]

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

Goal state before:
pp: F : Type u_1
Γ✝ : Subgroup (GL (Fin 2) ℝ)
k✝ : ℤ
inst✝¹ : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
f : ι → SlashInvariantForm Γ k
⊢ ↑s.card * k = ∑ i ∈ s, k

Tactic:
by simp

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

Goal state before:
pp: f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ f ∣[k] 1 = f

Tactic:
by simp

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 0 = 0

Tactic:
by simp

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

Goal state before:
pp: case inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
q : ℂ
hq : ‖q‖ < 1
hq' : q ≠ 0
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
· exact Periodic.qParam_right_inv hh.ne' hq' ▸
      hfper.differentiableAt_cuspFunction hh.ne' <| UpperHalfPlane.mdifferentiableAt_iff.mp <|
        hfhol ⟨_, Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq'⟩

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ 0 = ↑Nat.zero * k

Tactic:
by simp

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

Goal state before:
pp: ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : ι → ModularForm Γ k
⊢ ↑s.card * k = ∑ i ∈ s, k

Tactic:
by simp

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

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

Tactic:
ModularForm.toSlashInvariantForm_coe,

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

Goal state before:
pp: ⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ ρ ∈ 𝒟

Tactic:
constructor <;> norm_num [ρ, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg' : ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
⊢ 1 ≤ normSq ↑(g • z)

Tactic:
contrapose! hg₀'
    refine ⟨S * g, ?_⟩
    rw [mul_smul]
    exact im_lt_im_S_smul hg₀'

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

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
by
  simp_rw [eisensteinSeries]
  apply le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
    (Summable.tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
      (summable_norm_eisSummand hk z))

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

Goal state before:
pp: case inl
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ DifferentiableOn ℂ (fun z ↦ (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z | 0 < z.im}

pp: case inr
k : ℤ
⊢ DifferentiableOn ℂ (fun z ↦ (↑(0 0) * z + ↑(0 1)) ^ (-k)) {z | 0 < z.im}

Tactic:
· apply DifferentiableOn.zpow
    · fun_prop
    · left
      exact fun z hz ↦ linear_ne_zero ⟨z, hz⟩
        ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)

Goal state after:
case inr
k : ℤ
⊢ DifferentiableOn ℂ (fun z ↦ (↑(0 0) * z + ↑(0 1)) ^ (-k)) {z | 0 < z.im}
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)

Tactic:
obtain ⟨C, hC⟩ := ModularFormClass.exists_petersson_le hk Γ f f
  refine ⟨C.sqrt, fun τ ↦ ?_⟩
  lift k to ℕ using hk
  specialize hC τ
  have hC' : 0 ≤ C := le_trans (by positivity) <| (div_le_iff₀ (by positivity)).mpr hC
  have h : 0 < ‖(τ.im : ℂ) ^ (k : ℤ)‖ := mod_cast norm_pos_iff.mpr (pow_ne_zero _ τ.im_ne_zero)
  rw [petersson, norm_mul, norm_mul, Complex.norm_conj, ← sq, ← le_div_iff₀ h, mul_div_assoc] at hC
  rw [← sq_le_sq₀ (by positivity) (by positivity), mul_pow, sq_sqrt hC']
  refine hC.trans (congrArg (C * ·) ?_).le
  -- remains to show `(max τ.im (1 / τ.im)) ^ k / ‖τ.im ^ k‖ = (max 1 (1 / τ.im ^ k)) ^ 2`,
  -- which is easier after lifting to `NNReal`
  generalize h : τ.im = t
  have ht : 0 < t := h ▸ τ.im_pos
  lift t to NNReal using ht.le
  rw [← coe_nnnorm]
  norm_cast at ⊢ ht
  rw [(pow_left_mono k).map_max, (pow_left_mono 2).map_max, ← max_div_div_right (by positivity)]
  congr <;> simp [field, ht.ne']

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ 1 - 0 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
x✝¹ : ↥(↑b).divisorsAntidiagonal
x✝ : x✝¹ ∈ (↑b).divisorsAntidiagonal.attach
⊢ 0 ≤ ‖↑(↑x✝¹).2‖ ^ k

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
x✝¹ : ↥(↑b).divisorsAntidiagonal
x✝ : x✝¹ ∈ (↑b).divisorsAntidiagonal.attach
⊢ 0 ≤ ‖r‖ ^ ((↑x✝¹).1 * (↑x✝¹).2)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k m : ℕ
inst✝ : NeZero m
⊢ 0 ≤ ‖r‖

Tactic:
by simp

Goal state after:
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
⊢ 𝓝 0 = 𝓝 ((1 - 0)⁻¹ - 1)

Tactic:
by simp

Goal state after:
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
⊢ 1 - 0 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: z : ℍ
⊢ Even 2

Tactic:
by simp

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

Goal state before:
pp: z : ℍ
⊢ G2 z = ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]

Tactic:
set t := ∑' m, ∑' n, (G2Term z ![m, n])
  rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]
  · rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
    · congr with a
      rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
      exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])
    · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
        using (G2Term_prod_summable z).prod
  · exact (G2Term_prod_summable z).prod
  · exact summable_zero.congr
      fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by simp

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

Goal state before:
pp: case e_a
z : ℍ
⊢ 𝕢 24 ↑z ^ 24 = 𝕢 1 ↑z

Tactic:
simp [Periodic.qParam, ← exp_nsmul, nsmul_eq_mul, Nat.cast_ofNat]
    grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ‖ ≤ 1
⊢ !![0, -1; 1, 1].det = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S * T) 1 0
hc : ↑(T * S * T) 1 0 = 1
hd : ↑(T * S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ‖ ≤ 1
⊢ !![1, 0; 1, 1].det = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
⊢ !![0, -1; 1, -1].det = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : 1 = -↑z * ↑z
⊢ z = I

Tactic:
neg_mul,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : 1 = -(↑z * ↑z)
⊢ z = I
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N

Tactic:
neg_mul,

Goal state after:
z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n - ↑z / -↑↑N =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-(2 * ↑π) * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∀ (b : (r : ℕ) × ↑(gammaSet 1 r 0)),
    ((fun x ↦ eisSummand (↑k) x z) ∘ ⇑gammaSetDivGcdSigmaEquiv.symm) b = eisSummand (↑k) (↑b.snd) z

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: this : IsClosed {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
x✝ : x ∈ {z | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
him : 0 ≤ x.im
hre : 1 ≤ ‖x‖
hnorm : |x.re| ≤ 1 / 2
⊢ x.im ≠ 0

Tactic:
grind [abs_re_eq_norm]

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

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

Tactic:
neg_mul,

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n =
    1 + -(2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑↑n)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ 𝒟ᵒ = interior 𝒟

Tactic:
by
  refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_
  have ho1 := isOpenMap_re.image_interior_subset 𝒟
  have ho2 := isOpenMap_norm.image_interior_subset 𝒟
  intro x hx
  rw [Set.image_subset_iff] at *
  constructor
  · rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]
    apply Set.mem_of_mem_of_subset (Set.mem_preimage.mp (ho2 hx)) (interior_mono ?_)
    rw [Set.image_subset_iff]
    intro ξ hξ
    simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1
  · rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]
    apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)
    rw [Set.image_subset_iff]
    intro ξ hξ
    simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)

Goal state after:
case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ≤ y
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
j : GL (Fin 2) ℝ
hj : j ∈ 𝒢
hj' : ↑h' = ↑h * j
⊢ (⇑f ∣[k] (↑h)⁻¹) τ = (⇑f ∣[k] (↑h')⁻¹) τ

Tactic:
simp [hj', SlashAction.slash_mul, SlashInvariantFormClass.slash_action_eq f j⁻¹ (inv_mem hj)]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
t : ℝ
ht : 0 < t
⊢ 0 <
    ↑(Matrix.GeneralLinearGroup.det
        (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))

Tactic:
by simp

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
c : ℂ
hc : ⇑(ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) = Function.const ℍ c
⊢ ((⇑f - Function.const ℍ (f I)) ∣[0] ((Matrix.SpecialLinearGroup.mapGL ℝ) 1)⁻¹) I = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s}))
      (∑ x ∈ range p, (a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x + a ^ x * a ^ (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ x * a ^ (p - 1 - x))

Tactic:
sum_add_distrib,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ (Ideal.Quotient.mk (span {s}))
      (∑ x ∈ range p, a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x + ∑ x ∈ range p, a ^ x * a ^ (p - 1 - x)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ x * a ^ (p - 1 - x))
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x y : K
⊢ { toCompletion := ↑(WithAbs.toAbs (↑v) (x + y)) } =
    { toCompletion := ↑(WithAbs.toAbs (↑v) x) } + { toCompletion := ↑(WithAbs.toAbs (↑v) y) }

Tactic:
ext; simp [UniformSpace.Completion.coe_add]

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulOneClass (G i)
inst✝¹ : ∀ (i : ι), OneMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r s : G i
i✝ : ι
⊢ (mulSingle A i (r * s)) i✝ = (mulSingle A i r * mulSingle A i s) i✝

Tactic:
simp [Pi.mulSingle_mul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
n d : R
hd : d ∈ nonZeroDivisors R
hd' : d ≠ 0
this✝ : {v | (valuation K v) ((algebraMap R K) d) < 1}.Finite
v : HeightOneSpectrum R
hv : v ∈ Support R k
hk : (valuation K v) k * v.intValuation d = v.intValuation n
this : 1 ≤ v.intValuation d
⊢ 0 < 1

Tactic:
by simp

Goal state after: