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

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
hc : 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 = ρ

Tactic:
im_smul_eq_div_normSq,

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = z.im
hc : 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 = ρ
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
⊢ k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * ↑π * I) ^ (k + 1)

Tactic:
rw [← neg_pow]; ring

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

Goal state before:
pp: case h.inl.«1»
k : ℕ
ihn :
  ∀ m < 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 1
hk : 1 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑1) =
    ↑(if 1 ≡ 2 [MOD 12] then 1 / 12 else 1 / 12 + 1)

Tactic:
grind

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

Goal state before:
pp: k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ k ∈ Finset.filter Even (Finset.Icc 3 11)

Tactic:
grind

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

Goal state before:
pp: z : ℍ
a b : ℤ
this : Summable fun x ↦ (↑b - ↑a) * ((↑↑x * ↑z + ↑a) * (↑↑x * ↑z + ↑b))⁻¹
m : { x // x ∉ {0} }
⊢ ↑m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0

Tactic:
grind

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

Goal state before:
pp: z : ℍ
m : ℤ
this : Summable fun x ↦ ((↑m * ↑z + ↑↑x + 1) * (↑m * ↑z + ↑↑x))⁻¹
b : { x // x ∉ {0, -1} }
⊢ m ≠ 0 ∨ ↑b ≠ 0 ∧ ↑b + 1 ≠ 0

Tactic:
grind

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

Goal state before:
pp: k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
⊢ Even (k - 12)

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ k ≠ 0

Tactic:
grind

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

Goal state before:
pp: case pos
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
h✝ : k % 12 = 2 % 12
⊢ 1 + ↑((k - 12) / 12) = ↑((k - 12) / 12 + 1)

Tactic:
grind

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

Goal state before:
pp: case neg
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 12 ≤ k
h✝ : ¬k % 12 = 2 % 12
⊢ 1 + ↑((k - 12) / 12 + 1) = ↑((k - 12) / 12 + 1 + 1)

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 1 ≤ k - 1

Tactic:
grind

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

Goal state before:
pp: case h.inl
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : k < 12
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
apply rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero (by lia))

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 : I = z ∨ ↑I = -↑z
⊢ z = I

Tactic:
grind

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

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

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
hg : g • I = I
this : (g = 1 ∨ g = -1) ∨ g = S ∨ g = -S
⊢ g ∈ {1, -1, S, -S}

Tactic:
grind

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

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (b : ℕ+), ((-↑↑d + ↑↑b * ↑z)⁻¹ - (↑↑d + ↑↑b * ↑z)⁻¹ + ((-↑↑d - ↑z * ↑↑b)⁻¹ - (↑↑d - ↑z * ↑↑b)⁻¹)) =
    ∑' (m : ℕ+), ((-↑↑d + ↑z * ↑↑m)⁻¹ + (-↑↑d - ↑z * ↑↑m)⁻¹ - (↑↑d + ↑z * ↑↑m)⁻¹ - (↑↑d - ↑z * ↑↑m)⁻¹)

Tactic:
grind

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

Goal state before:
pp: 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
⊢ 2 ≤ k

Tactic:
grind

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

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

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
this : (g = 1 ∨ g = -1) ∨ (g = S * T ∨ g = -(S * T)) ∨ g = T⁻¹ * S ∨ g = -(T⁻¹ * S)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ 1 < k

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : 1 • z ∈ 𝒟ᵒ
⊢ ↑1 1 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ ↑(-1) 1 0 = 0

Tactic:
rfl

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

Goal state before:
pp: z : ℍ
N : ℕ+
i : ℤ
hi : i ∈ Ico (-↑↑N) ↑↑N
⊢ ∀ (b : ℤ), 1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑(i + 1)) = 1 / (↑b * ↑z + ↑i) - 1 / (↑b * ↑z + ↑i + 1)

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z =
    2 * riemannZeta ↑k +
      2 * ((-2 * ↑π * I) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
⊢ 1 < k

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
z2 : riemannZeta ↑k ≠ 0
HE1 :
  ∑' (v : Fin 2 → ℤ), ((↑(v 0) * ↑z + ↑(v 1)) ^ k)⁻¹ =
    2 * riemannZeta ↑k +
      2 * ((-(2 * ↑π * I)) ^ k / ↑(k - 1)!) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
HE2 :
  (riemannZeta ↑k)⁻¹ * ∑' (v : Fin 2 → ℤ), ((↑(v 0) * ↑z + ↑(v 1)) ^ k)⁻¹ =
    ∑' (x : ↑(gammaSet 1 1 0)), ((↑(↑x 0) * ↑z + ↑(↑x 1)) ^ k)⁻¹
⊢ 2⁻¹ * ∑' (x : ↑(gammaSet 1 1 0)), ((↑(↑x 0) * ↑z + ↑(↑x 1)) ^ k)⁻¹ =
    1 +
      (riemannZeta ↑k)⁻¹ * (-(2 * ↑π * I)) ^ k / ↑(k - 1)! *
        ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
⊢ k = 2 * (k / 2 - 1 + 1)

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ m + 1 ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (UpperHalfPlane.coe ∘ fun t ↦ ↑ofComplex (↑t * ↑x)) (𝓝 1) (𝓝 ↑x)

Tactic:
Function.comp_def

Goal state after:
case hf
x : ℍ
hxnorm : 1 < ‖↑x‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun x_1 ↦ ↑(↑ofComplex (↑x_1 * ↑x))) (𝓝 1) (𝓝 ↑x)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ 2 * (m + 1) - 1 = 2 * m + 1

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ 2 ^ (2 * (m + 1)) * (-1) ^ (m + 1) / ↑(bernoulli (2 * (m + 1))) =
    -(2 * (-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) / ↑(bernoulli (2 * (m + 1))))

Tactic:
grind

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ k ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ (γ • τ).im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
im_smul_eq_div_normSq,

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
h1 : τ.im ≤ τ.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ)
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
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
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
⊢ quotientFunc f q ∣[k] h = quotientFunc f (⟨h, hh⟩⁻¹ • q)

Tactic:
induction q using Quotient.inductionOn with
  | h r => simp [SlashAction.slash_mul]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), {g | g ∈ H ∧ (g • t • K ∩ L).Nonempty}.Finite
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G)) S
hT : (Subtype.val '' S).Finite
hS' : ∀ {g : Γ}, g ∈ G → ∃ t ∈ Subtype.val '' S, g * t⁻¹ ∈ H
g : Γ
⊢ g ∈ G → (g • K ∩ L).Nonempty → ∃ i, g * i⁻¹ ∈ H ∧ (∃ (x : i ∈ G), ⟨i, ⋯⟩ ∈ S) ∧ (g • K ∩ L).Nonempty

Tactic:
grind

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
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 *
      ((Ideal.Quotient.mk (span {s})) b *
        ((Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) * (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2))) =
    0

Tactic:
refine mul_eq_zero_of_left ?_ _

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
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 = 0
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
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ 0 ≤ 2 * ↑n

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℕ
⊢ (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_2.zero
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ 0 + y ^ 2 ^ 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd y

Tactic:
convert! Even.add_odd hxy hx

Goal state after:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ y = -(x - y) + x
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case e'_3.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity ↑2 ↑n = emultiplicity 2 ↑n

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ∣ x - 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : realMixedSpace K → E
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, (x.2 w).1) • f (↑(polarCoordReal K).symm x) = (∏ x_1, |(x.2 x_1).1|) • f (↑(polarCoordReal K).symm x)

Tactic:
abs_of_mem_polarCoordReal_target K hx

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    (∏ i, ENNReal.ofReal |(x.2 i).1|) * f (↑(polarCoordReal K).symm x)

Tactic:
abs_of_mem_polarCoordReal_target K hx

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
this :
  (Subgroup.map (QuotientGroup.mk' (torsion K)) (Subgroup.closure (Set.range u))).index =
    (Subgroup.closure (Set.range u) ⊔ torsion K).index
⊢ (AddSubgroup.map (↑(logEmbeddingEquiv K).toAddEquiv)
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0 ↔
    (AddSubgroup.map (↑↑(logEmbeddingEquiv K))
          (AddSubgroup.closure (⇑Additive.toMul.symm '' QuotientGroup.mk '' Set.range u))).index ≠
      0

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm) x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))

Tactic:
Function.comp_def

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((fun x ↦ (mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x)) x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f ((⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm) x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))

Tactic:
Function.comp_def

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) *
        f ((fun x ↦ (mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x)) x) =
    ∫⁻ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ⇑mixedSpaceOfRealSpace ⁻¹' A =ᵐ[Measure.pi fun x ↦ volume] ⇑mixedSpaceOfRealSpace ⁻¹' A

Tactic:
rfl

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ (algebraMap (↥K⁺) K) ⟨↑x, h⟩ = ↑x

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e'_3.e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w₁ w₂ : InfinitePlace K
e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)
e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)
g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm
h_col :
  |((of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm))
          id).det| =
    |(of fun i w ↦ ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
h :
  |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| =
    |((of fun i w ↦ ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id
          (f.symm w₂).succAbove).det|
i✝ j✝ : Fin (rank K)
⊢ ↑(↑(g.symm j✝)).mult * Real.log (↑(g.symm j✝) ((algebraMap (𝓞 K) K) ↑(u i✝))) =
    ↑(f ((f.symm w₂).succAbove j✝)).mult * Real.log ((f ((f.symm w₂).succAbove j✝)) ((algebraMap (𝓞 K) K) ↑(u i✝)))

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (mixedEmbedding K).toIntAlgHom ↑y = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
RingHom.toIntAlgHom_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (mixedEmbedding K) ↑y = x) ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝² : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ ≤ ⌊s⌋₊) ∧ absNorm ↑x✝ = i ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = i

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // intNorm ↑((idealSetEquiv K J) a) = i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ ↑(f.symm w) = (equivInfinitePlace K).symm ↑w

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
i w : { w // w ≠ w₀ }
⊢ (algebraMap (𝓞 K) K) ↑(realFundSystem K (g.symm (f.symm i))) = (algebraMap (↥K⁺) K) ?m.301

Tactic:
rfl

Goal state after: