mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
qExpansion_coeff_eq_circleIntegral hh hfper hfhol hfbdd n hR0 hR1,

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
⊢ (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) j

case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case «0»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.«0».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«0».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case h.«1».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«1».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case h.«0».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«0».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case h.«1».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«1».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(T ^ ↑g 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case h.«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) j

case h.«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«0»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«1»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«0»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case pos.«_@».Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs.1971615608._hygCtx._hyg.42.«1»
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
⊢ v ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h.«0».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«0».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case h.«1».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«1».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case h.«0».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«0».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case h.«1».«0»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«1».«1»
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = ↑(-T ^ (-↑g 0 1)) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case «0»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
⊢ 1 ≤ normSq ↑ρ

pp: case right
⊢ |ρ.re| ≤ 1 / 2

Tactic:
<;>

Goal state after:
case left
⊢ 1 ≤ normSq ↑ρ

case right
⊢ |ρ.re| ≤ 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
⊢ 1 ≤ normSq ↑I

pp: case right
⊢ |I.re| ≤ 1 / 2

Tactic:
<;>

Goal state after:
case left
⊢ 1 ≤ normSq ↑I

case right
⊢ |I.re| ≤ 1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h✝ : |z.re| = z.re ∧ 0 ≤ z.re
⊢ 3 < 4 * z.im ^ 2

pp: case inr
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h✝ : |z.re| = -z.re ∧ z.re < 0
⊢ 3 < 4 * z.im ^ 2

Tactic:
<;>

Goal state after:
case inl
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h✝ : |z.re| = z.re ∧ 0 ≤ z.re
⊢ 3 < 4 * z.im ^ 2

case inr
z : ℍ
h : z ∈ 𝒟ᵒ
this✝ : 1 < z.re * z.re + z.im * z.im
this : |z.re| < 1 / 2
h✝ : |z.re| = -z.re ∧ z.re < 0
⊢ 3 < 4 * z.im ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = τ.re ∧ 0 ≤ τ.re
⊢ 3 ≤ 4 * τ.im ^ 2

pp: case inr
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = -τ.re ∧ τ.re < 0
⊢ 3 ≤ 4 * τ.im ^ 2

Tactic:
<;>

Goal state after:
case inl
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = τ.re ∧ 0 ≤ τ.re
⊢ 3 ≤ 4 * τ.im ^ 2

case inr
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
h✝ : |τ.re| = -τ.re ∧ τ.re < 0
⊢ 3 ≤ 4 * τ.im ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
⊢ |(g • z).re + 1| < |(g • z).re|

pp: case right.left.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
<;>

Goal state after:
case right.left.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
⊢ |(g • z).re + 1| < |(g • z).re|

case right.left.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
⊢ |(g • z).re + 1| < |(g • z).re|
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.left.inl.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

pp: case right.left.inl.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|

pp: case right.left.inr.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

pp: case right.left.inr.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|

Tactic:
<;>

Goal state after:
case right.left.inl.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

case right.left.inl.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = (g • z).re + 1 ∧ 0 ≤ (g • z).re + 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|

case right.left.inr.inl
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re + 1| < |(g • z).re|

case right.left.inr.inr
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' • z).im ≤ (g • z).im
hg' : (g • z).re < -(1 / 2)
h✝¹ : |(g • z).re + 1| = -((g • z).re + 1) ∧ (g • z).re + 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re + 1| < |(g • z).re|
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
⊢ |(g • z).re - 1| < |(g • z).re|

pp: case right.right.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
<;>

Goal state after:
case right.right.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
⊢ |(g • z).re - 1| < |(g • z).re|

case right.right.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
⊢ |(g • z).re - 1| < |(g • z).re|
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right.inl.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

pp: case right.right.inl.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|

pp: case right.right.inr.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

pp: case right.right.inr.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
<;>

Goal state after:
case right.right.inl.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

case right.right.inl.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|

case right.right.inr.inl
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = (g • z).re ∧ 0 ≤ (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|

case right.right.inr.inr
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' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
h✝¹ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
h✝ : |(g • z).re| = -(g • z).re ∧ (g • z).re < 0
⊢ |(g • z).re - 1| < |(g • z).re|
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.h
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
this : c ≠ 0 → 9 * c ^ 4 ≤ 16
hc : c ≠ 0
⊢ (3 * c ^ 2) ^ 2 ≤ 4 ^ 2

pp: case hb
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
this : c ≠ 0 → 9 * c ^ 4 ≤ 16
hc : c ≠ 0
⊢ 0 ≤ 4

Tactic:
<;>

Goal state after:
case inr.h
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
this : c ≠ 0 → 9 * c ^ 4 ≤ 16
hc : c ≠ 0
⊢ (3 * c ^ 2) ^ 2 ≤ 4 ^ 2

case hb
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
this : c ≠ 0 → 9 * c ^ 4 ≤ 16
hc : c ≠ 0
⊢ 0 ≤ 4
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h₁
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
hc : c ≠ 0
⊢ 3 ≤ 4 * (g • z).im ^ 2

pp: case h₂
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
hc : c ≠ 0
⊢ 3 ≤ 4 * z.im ^ 2

Tactic:
<;>

Goal state after:
case h₁
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
hc : c ≠ 0
⊢ 3 ≤ 4 * (g • z).im ^ 2

case h₂
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ⋯
c : ℝ := ⋯
hc : c ≠ 0
⊢ 3 ≤ 4 * z.im ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = T ∨ g = -T ↔ -g = T ∨ -g = -T

pp: case e'_2.e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ↔ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2

pp: case e'_2.e'_2
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = 1 ∨ g = -1 ↔ -g = 1 ∨ -g = -1

Tactic:
<;>

Goal state after:
case e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = T ∨ g = -T ↔ -g = T ∨ -g = -T

case e'_2.e'_1
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ↔ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2

case e'_2.e'_2
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ g = 1 ∨ g = -1 ↔ -g = 1 ∨ -g = -1
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ max t (1 / t) ^ k / ‖↑(t ^ k)‖₊ = max 1 (1 / t ^ k) ^ 2

Tactic:
rw [(pow_left_mono k).map_max, (pow_left_mono 2).map_max, ← max_div_div_right (by positivity)]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ max (t ^ k / ‖↑(t ^ k)‖₊) ((1 / t) ^ k / ‖↑(t ^ k)‖₊) = max (1 ^ 2) ((1 / t ^ k) ^ 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case «1»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
j : Fin 2
⊢ ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, b; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: case e_a
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ t ^ k / ‖↑(t ^ k)‖₊ = 1 ^ 2

pp: case e_a
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ (1 / t) ^ k / ‖↑(t ^ k)‖₊ = (1 / t ^ k) ^ 2

Tactic:
<;>

Goal state after:
case e_a
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ t ^ k / ‖↑(t ^ k)‖₊ = 1 ^ 2

case e_a
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < t
⊢ (1 / t) ^ k / ‖↑(t ^ k)‖₊ = (1 / t ^ k) ^ 2