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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ↑N ^ (-(1 - s)) *
      ∑ x,
        Φ x *
          (C *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * C *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc,
    neg_sub]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ C *
      (↑N ^ (s - 1) *
        ∑ x,
          Φ x *
            (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s +
              cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s)) =
    C *
      (↑N ^ (s - 1) *
        (cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ (2 * ↑k).Gammaℂ * Complex.cos (↑π * (2 * ↑k) / 2) * cosZeta (↑x) (2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
cosZeta_two_mul_nat' hk hx,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ (2 * ↑k).Gammaℂ * Complex.cos (↑π * (2 * ↑k) / 2) *
      ((-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
        Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m :
  bernoulliFun k 1 =
    2 ^ k / 2 *
      (∑ x ∈ Finset.range 0, bernoulliFun k (2⁻¹ + ↑x / 2) + bernoulliFun k (2⁻¹ + ↑0 / 2) +
        bernoulliFun k (2⁻¹ + ↑1 / 2))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
Finset.sum_range_zero,

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k 1 = 2 ^ k / 2 * (0 + bernoulliFun k (2⁻¹ + ↑0 / 2) + bernoulliFun k (2⁻¹ + ↑1 / 2))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case refine_1.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ s ≠ 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

pp: case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s

Tactic:
· exact fun h ↦ (differentiableAt_const _).div differentiableAt_id h

Goal state after:
case refine_1.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ Φ 0 = 0 → DifferentiableAt ℂ (HDiv.hDiv (Φ 0)) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ (↑q.totient)⁻¹ / (↑x - 1) = ↑((↑q.totient)⁻¹ / (↑x - 1)).re

Tactic:
rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]

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

Goal state before:
pp: case refine_4
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ IntegrableAtFilter (fun t ↦ t ^ (-(s.re + 1) + r)) atTop volume

Tactic:
integrableAtFilter_rpow_atTop_iff,

Goal state after:
case refine_4
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ -(s.re + 1) + r < -1
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) *
      ↑(Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val).prod =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!

Tactic:
← Finset.prod_eq_multiset_prod,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(∏ x ∈ Ico 1 (p / 2).succ, x) =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ IntegrableAtFilter (fun t ↦ t ^ (-s)) atTop volume

Tactic:
integrableAtFilter_rpow_atTop_iff,

Goal state after:
case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ -s < -1
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
⊢ IsDiscrete R

Tactic:
by_cases H : DenselyOrdered (ValueGroupWithZero R)

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

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

Tactic:
let e : (R ⧸ I) ≃ₗ[R] R ⧸ (LinearMap.ker (f.comp g)) :=
    Submodule.quotEquivOfEq I (LinearMap.ker (f ∘ₗ g)) this

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

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : ↥𝒪[K]
⊢ ↑(Ideal.span {x}) = Metric.closedBall 0 ‖x‖

Tactic:
simp [Valuation.integer.coe_span_singleton_eq_setOfPred_le_v_coe, Set.ext_iff,
    ← NNReal.coe_le_coe]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

pp: case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1

Tactic:
· exact Nat.mod_two_ne_zero.mp hb2

Goal state after:
case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
exact LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₂ h₀ hε hs hT₁
        fun t ht ↦ (hT t ht.le).le

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_2
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
⊢ (ofFn (n + 1)) ↑p ∈ boxPoly n B₁ B₂

pp: case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

pp: case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

Tactic:
· refine ⟨Nat.le_of_lt_succ <| ofFn_natDegree_lt (Nat.le_add_left 1 n) p.val, fun i ↦ ?_⟩
      have prop := Finset.mem_Icc.mp p.property
      rw [ofFn_coeff_eq_val_of_lt _ i.2]
      exact ⟨ceil_le.mp (prop.1 i), le_floor.mp (prop.2 i)⟩

Goal state after:
case refine_3
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.LeftInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
⊢ ∃ n, 0 < n ∧ z ^ n = 1

Tactic:
let K := ℚ⟮z⟯
  let : NumberField K := {
    to_charZero := ℚ⟮z⟯.charZero,
    to_finiteDimensional := adjoin.finiteDimensional
      (isIntegral_of_mahlerMeasure_eq_one h hz).tower_top }
-- `y` is `z` as an element of `K`
  let y : K := ⟨z, mem_adjoin_simple_self ℚ z⟩
  suffices ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1 by
    obtain ⟨n, hn₀, hn₁⟩ := this
    exact ⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩
  refine NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_
  rw [mem_aroots] at hz ⊢
  refine ⟨hz.1, ?_⟩
  have H (ψ : K →+* ℂ) : ψ ((aeval y) p) = (aeval (ψ y)) p := by
    conv_rhs => rw [← map_id (p := p)]
    exact p.map_aeval_eq_aeval_map (by ext; simp) y
  rw [← H, map_eq_zero_iff _ φ.injective,
    ← map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ↥K ℂ), H]
  exact hz.2

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
by
  have pow2 : (2 : ZMod q) ^ ((q + 1) / 2) = 2 := by
    obtain ⟨_, _⟩ := odd
    rw [(by lia : (q + 1) / 2 = q / 2 + 1), pow_succ]
    have leg := legendreSym.eq_pow q 2
    have : (2 : ZMod q) = ((2 : ℤ) : ZMod q) := by norm_cast
    rw [this, ← leg, leg2]
    ring
  have := two_mul_ω_pow odd leg3
  rw [mul_pow] at this
  have coe : (2 : X q) = (2 : ZMod q) := by rw [map_ofNat]
  rw [coe, ← map_pow, pow2, ← coe,
    (by ring : (-2 : X q) = 2 * -1)] at this
  refine (IsUnit.of_mul_eq_one (M := X q) ↑((q + 1) / 2) ?_).mul_left_cancel this
  norm_cast
  simp [Nat.mul_div_cancel' odd.add_one.two_dvd]

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ, y = g * x * g⁻¹) ↔ x ∈ toConjAct g⁻¹ • Γ

Tactic:
exists_eq_right,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ g * x * g⁻¹ ∈ Γ ↔ x ∈ toConjAct g⁻¹ • Γ
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case h
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
⊢ (y - 1) i j = ↑a₁ * ↑a₂ * ↑M * ((y - 1) i j / (↑a₁ * ↑a₂ * ↑M))

Tactic:
refine (Int.mul_ediv_cancel_of_dvd ?_).symm

Goal state after:
case h
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
⊢ ↑a₁ * ↑a₂ * ↑M ∣ (y - 1) i j
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
g : GL (Fin 2) R
v : R × R
⊢ g • v = (↑g 0 0 * v.1 + ↑g 0 1 * v.2, ↑g 1 0 * v.1 + ↑g 1 1 * v.2)

Tactic:
simp [Units.smul_def, Matrix.fin_two_smul_prod]

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ A) ((σ B) (f ((A * B) • τ))) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) * denom (A * B) ↑τ ^ (-k) =
    (σ A) ((σ B) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))

Tactic:
denom_cocycle_σ,

Goal state after:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ A) ((σ B) (f ((A * B) • τ))) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) *
      ((σ B) (denom A ↑(B • τ)) * denom B ↑τ) ^ (-k) =
    (σ A) ((σ B) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N,
    N ≠ 0 ∧
      toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
obtain ⟨N, hN, h⟩ := exists_Gamma_le_conj g M
  refine ⟨N, hN, fun y hy ↦ ?_⟩
  simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.mem_map,
    eq_inv_smul_iff] at hy
  obtain ⟨x, hx, rfl⟩ := hy
  obtain ⟨z, hz, hz'⟩ := h x hx
  use z, hz
  simpa only [Subtype.ext_iff, Units.ext_iff, map_mul] using!
    congr_arg (GeneralLinearGroup.map (Rat.castHom ℝ)) hz'

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

Goal state before:
pp: case mpr
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → IsCusp c (mapGL ℝ).range

Tactic:
· rintro ⟨c, rfl⟩
    obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ
    refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
    · suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
      refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
      simp [discr_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]
      norm_num
    · rw [← Rat.coe_castHom, ← (Rat.castHom ℝ).algebraMap_toAlgebra]
      simp [OnePoint.map_smul, mul_smul, smul_infty_eq_self_iff, ModularGroup.T]

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

Goal state before:
pp: case refine_2
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
⊢ rexp (-π) < 1

pp: case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w ∈ Metric.closedBall 0 (rexp (-π)), ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

Tactic:
· simp [pi_pos]

Goal state after:
case refine_3
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ ∃ w ∈ Metric.closedBall 0 (rexp (-π)), ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (↑(T ^ n • z)).re = z.re + ↑n

Tactic:
coe_T_zpow_smul_eq,

Goal state after:
z : ℍ
n : ℤ
⊢ (↑z + ↑n).re = z.re + ↑n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (↑(T ^ n • z)).im = z.im

Tactic:
coe_T_zpow_smul_eq,

Goal state after:
z : ℍ
n : ℤ
⊢ (↑z + ↑n).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
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
⊢ |(g • z).re| ≤ 1 / 2

Tactic:
· change |(g • z).re| ≤ 1 / 2
    -- if not, then either `T` or `T'` decrease |Re|.
    rw [abs_le]
    constructor
    · contrapose! hg'
      refine ⟨T * g, (T_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_smul]
      cases abs_cases ((g • z).re + 1) <;> cases abs_cases (g • z).re <;> linarith
    · contrapose! hg'
      refine ⟨T⁻¹ * g, (T_inv_mul_apply_one _).symm, ?_⟩
      rw [mul_smul, re_T_inv_smul]
      cases abs_cases ((g • z).re - 1) <;> cases abs_cases (g • z).re <;> linarith

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
hgz : g = T ^ b
⊢ (↑(T ^ b • z)).re = ↑b + z.re

Tactic:
coe_T_zpow_smul_eq,

Goal state after:
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
hgz : g = T ^ b
⊢ (↑z + ↑b).re = ↑b + z.re
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
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
hgz : g = T ^ 1
hre : (g • z).re = ↑b + z.re
hb : b = 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

pp: case inr.inr
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
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
· left
    rw [hgz, zpow_one, eq_self_iff_true, true_or, true_and]
    rw [hb, Int.cast_one] at hre
    linarith [(le_abs_self _).trans (abs_neg z.re ▸ hz.2), (le_abs_self _).trans hg.2]

Goal state after:
case inr.inr
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
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑(T ^ ↑g 0 0 • S • z)).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
coe_T_zpow_smul_eq,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this : |(↑(S • z) + ↑(↑g 0 0)).re| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.Modular

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

Tactic:
have hρ : z = (1 : ℝ) +ᵥ ρ := by
    apply eq_of_re_of_norm
    · norm_num [h', ρ]
    · rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]

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

Goal state before:
pp: ⊢ Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) = 1

Tactic:
simpa [CuspForm.discriminantEquiv.rank_eq] using! levelOne_weight_zero_rank_one

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

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
⊢ qExpansion 1 ⇑f = 0

Tactic:
obtain ⟨c6, hc6⟩ : ∃ c6, c6 • E₆ = (f.mul f).mul f :=
    (finrank_eq_one_iff_of_nonzero' E₆ (E_ne_zero _ ⟨3, rfl⟩)).mp
      (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_six_rank_one) _

Goal state after:
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ qExpansion 1 ⇑f = 0
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 * ↑z + ↑↑b + 1) * (↑m * ↑z + ↑↑b))⁻¹ = 1 / (↑m * ↑z + ↑↑b) - 1 / (↑m * ↑z + ↑↑b + 1)

Tactic:
simpa [add_assoc, mul_comm] using
    (one_div_linear_sub_one_div_linear_eq z b (b + 1) m (by grind)).symm

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

Goal state before:
pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
rw [levelOne_odd_weight_rank_zero hk_odd]
    exact Cardinal.aleph0_pos

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ ∑' (c : ℤ), eisSummand ↑k ![(-n, c).1, (-n, c).2] z = ∑' (c : ℤ), eisSummand ↑k ![(n, c).1, (n, c).2] z

Tactic:
nth_rewrite 1 [← tsum_comp_neg]

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
n : ℤ
⊢ ∑' (d : ℤ), eisSummand ↑k ![(-n, -d).1, (-n, -d).2] z = ∑' (c : ℤ), eisSummand ↑k ![(n, c).1, (n, c).2] z