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

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

pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 +ᵥ ρ
this✝ : S • ρ = T • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
h : ↑g 0 0 = -1
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

Tactic:
<;>

Goal state after:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 +ᵥ ρ
this✝ : S • ρ = T • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
h : ↑g 0 0 = 0
⊢ T ^ ↑g 0 0 * S * T⁻¹ = S * T⁻¹ ∨ T ^ ↑g 0 0 * S * T⁻¹ = T⁻¹ * S * T⁻¹

case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (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 +ᵥ ρ
this✝ : S • ρ = T • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
h : ↑g 0 0 = -1
⊢ 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: case inl.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
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
⊢ (g • z).im = z.im

pp: case inl.inr.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
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g • z).im = z.im

pp: case inl.inr.inr.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
h : g = 1
⊢ (g • z).im = z.im

pp: case inl.inr.inr.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 = 0
h : g = -1
⊢ (g • z).im = z.im

Tactic:
<;>

Goal state after:
case inl.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
h : (g = T ∨ g = -T) ∧ z.re = -1 / 2
⊢ (g • z).im = z.im

case inl.inr.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
h : (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2
⊢ (g • z).im = z.im

case inl.inr.inr.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
h : g = 1
⊢ (g • z).im = z.im

case inl.inr.inr.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 = 0
h : g = -1
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.Modular

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

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

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

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

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

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

Tactic:
<;>

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

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

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

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

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

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

Goal state before:
pp: hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
hq_norm : ‖𝕢 1 ↑τ‖ = rexp (-2 * π * τ.im)
hsub : ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24 - 1‖ < 1 / 2
h1 : ‖1‖ - ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖ ≤ ‖1 - ∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖
⊢ 1 / 2 ≤ ‖∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24‖

Tactic:
grind [norm_one, norm_sub_rev]

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

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ ∑' (x : ℕ+), 2 * ((I * (↑π * 2)) ^ 2 * (cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑x * ↑↑x)) =
    -∑' (x : ℕ+), 8 * (↑π ^ 2 * (cexp (↑z * (I * ↑π) * 2) ^ ↑x * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑x) * ↑↑x)))

Tactic:
← tsum_neg,

Goal state after:
case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ ∑' (x : ℕ+), 2 * ((I * (↑π * 2)) ^ 2 * (cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑x * ↑↑x)) =
    ∑' (b : ℕ+), -(8 * (↑π ^ 2 * (cexp (↑z * (I * ↑π) * 2) ^ ↑b * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑b) * ↑↑b))))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • E hk) - qExpansion 1 ⇑f) = 0

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
FunLike.coe_smul,

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • ⇑(E hk)) - qExpansion 1 ⇑f) = 0

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
by
  have : iteratedDerivWithin k (fun z ↦ ((π * I) -
    (2 * π * I) * ∑' n : ℕ, cexp (2 * π * I * z) ^ n)) ℍₒ z =
    -(2 * π * I) * ∑' n : ℕ, iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * s) ^ n) ℍₒ z := by
    rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]
    · simp only [iteratedDerivWithin_tsum_cexp_eq, neg_mul]
    · exact (contDiffOn_tsum_cexp k).contDiffWithinAt (by simpa using z.2)
  have h : -(2 * π * I * (2 * π * I) ^ k) * ∑' (n : ℕ), n ^ k * cexp (2 * π * I * z) ^ n =
        -(2 * π * I) * ∑' n : ℕ, (2 * π * I * n) ^ k * cexp (2 * π * I * z) ^ n := by
    simp_rw [← tsum_mul_left]
    congr
    ext y
    ring
  simp only [this, neg_mul, pow_succ', h, neg_inj, mul_eq_mul_left_iff, mul_eq_zero,
    OfNat.ofNat_ne_zero, ofReal_eq_zero, Real.pi_ne_zero, or_self, I_ne_zero, or_false]
  congr
  ext n
  have := exp_nsmul' (p := 1) (a := 2 * π * I) (n := n)
  simp_rw [div_one] at this
  simpa [this, UpperHalfPlane.coe] using
    iteratedDerivWithin_cexp_aux k n 1 isOpen_upperHalfPlaneSet z.2

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)

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:
<;>

Goal state after:
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)

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)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case pos
k : ℕ
hk_even : Even ↑k
h✝ : k ≡ 2 [MOD 12]
⊢ ↑(k / 12) < Cardinal.aleph0

pp: case neg
k : ℕ
hk_even : Even ↑k
h✝ : ¬k ≡ 2 [MOD 12]
⊢ ↑(k / 12 + 1) < Cardinal.aleph0

Tactic:
<;>

Goal state after:
case pos
k : ℕ
hk_even : Even ↑k
h✝ : k ≡ 2 [MOD 12]
⊢ ↑(k / 12) < Cardinal.aleph0

case neg
k : ℕ
hk_even : Even ↑k
h✝ : ¬k ≡ 2 [MOD 12]
⊢ ↑(k / 12 + 1) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e'_2.a
z : ℂ
m : ℤ
b : ℕ
x✝ : ℤ
a✝ : x✝ ∈ Ico (-↑b) ↑b
⊢ 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑x✝ + 1) = 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑(x✝ + 1))

pp: case e'_3.e'_5
z : ℂ
m : ℤ
b : ℕ
⊢ 1 / (↑m * z - ↑b) = 1 / (↑m * z + ↑(-↑b))

Tactic:
<;>

Goal state after:
case e'_2.a
z : ℂ
m : ℤ
b : ℕ
x✝ : ℤ
a✝ : x✝ ∈ Ico (-↑b) ↑b
⊢ 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑x✝ + 1) = 1 / (↑m * z + ↑x✝) - 1 / (↑m * z + ↑(x✝ + 1))

case e'_3.e'_5
z : ℂ
m : ℤ
b : ℕ
⊢ 1 / (↑m * z - ↑b) = 1 / (↑m * z + ↑(-↑b))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
⊢ g • ρ = ρ ↔ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

Tactic:
constructor
  · intro hg
    have neS : g ≠ S ∧ g ≠ -S := by
      have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]
      grind [SL_neg_smul]
    have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹ := by
      have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
      have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
      grind [SL_neg_smul]
    have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T) := by
      have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
      grind [SL_neg_smul]
    have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)
    norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, norm_ρ, ρ, neS, neT, neTST] at this
    grind
  · suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]
    rw [mul_smul T⁻¹, inv_smul_eq_iff, ← eq_inv_smul_iff (g := S), S_inv, SL_neg_smul,
      mul_smul, eq_comm, and_self, modular_T_smul, modular_S_smul, UpperHalfPlane.ext_iff]
    norm_num [ρ, Complex.ext_iff, normSq, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

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

Tactic:
<;>

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

case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ ↑(-1) 1 0 = 0
Module: Mathlib.NumberTheory.Modular

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

pp: case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ z = -1 • z

Tactic:
<;>

Goal state after:
case inl
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : 1 • z ∈ 𝒟ᵒ
⊢ z = 1 • z

case inr
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : -1 • z ∈ 𝒟ᵒ
⊢ z = -1 • z
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case «0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
j : Fin 2
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
j : Fin 2
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
j : Fin 2
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨0, ⋯⟩) j =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
j : Fin 2
⊢ ↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (-ModularGroup.S)))
      ((fun i ↦ i) ⟨1, ⋯⟩) j =
    ↑((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
          (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) (-ModularGroup.S))))
      ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ⇑(ModularForm.norm ℋ f) = ⇑0
⊢ ⇑f = 0

Tactic:
coe_norm,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ∏ q, quotientFunc f q = ⇑0
⊢ ⇑f = 0
Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

Goal state before:
pp: case fst
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).1 v

pp: case snd
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).2 v

Tactic:
<;>

Goal state after:
case fst
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).1 v

case snd
K : Type u_1
inst✝ : Field K
x : K
v : { w // w.IsComplex }
⊢ ((mixedEmbedding K) x).2 v = ((ringEquiv_mixedSpace K) ((algebraMap K K∞) x)).2 v
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
⊢ ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {s})) (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:
← map_sum,

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 + 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
hv : v.IsComplex
⊢ Function.Surjective ⇑(extensionEmbedding v)

Tactic:
← RingHom.fieldRange_eq_top_iff

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange = ⊤
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case ih
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
a✝ : WithAbs ↑v
⊢ ((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion)) { toCompletion := ↑a✝ } =
    (extensionEmbedding v) { toCompletion := ↑a✝ }

Tactic:
simp [WithAbs.algebraMap_left_apply, WithAbs.algebraMap_right_apply,
        ← ComplexEmbedding.LiesOver.over (conjugate w.embedding) v.embedding]

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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ single A i (x i * r) = x * single A i r

Tactic:
by
  ext j
  rcases eq_or_ne i j with rfl | hne; · simp
  simp [single_eq_of_ne' A _ hne]

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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ single A i (r * x i) = single A i r * x

Tactic:
by
  ext j
  rcases eq_or_ne i j with rfl | hne; · simp
  simp [single_eq_of_ne' A _ hne]

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : w.IsReal
⊢ Continuous fun a ↦ a.1 ⟨w, h✝⟩

pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ Continuous fun a ↦ (a.2 ⟨w, ⋯⟩).1

Tactic:
<;>

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : w.IsReal
⊢ Continuous fun a ↦ a.1 ⟨w, h✝⟩

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ Continuous fun a ↦ (a.2 ⟨w, ⋯⟩).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hc : c ≠ 0
⊢ c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩
  convert! smul_mem_of_mem h (inv_ne_zero hc)
  rw [eq_inv_smul_iff₀ hc]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsReal
⊢ Module.finrank v.Completion w.Completion = 1

pp: case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
⊢ Module.finrank v.Completion w.Completion = 1

Tactic:
· have := LiesOver.extensionEmbedding_liesOver_of_isReal w hv
    rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal hv) (ringEquivRealOfIsReal
        (h.liesOver_isReal_over _ _ hv)) (RingHom.ext fun _ ↦ Complex.ofReal_inj.1 <| by simp),
      Module.finrank_self]

Goal state after:
case inr
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsUnramified K w
hv : v.IsComplex
⊢ Module.finrank v.Completion w.Completion = 1