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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
let U := {t : ℂ | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F = G * H

Tactic:
ext1 t

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
t : ℂ
⊢ B.F t = (G * H) t
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
neg_eq_neg_one_mul,

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
| 1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-1 * ↑↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) ↑(-2) = 0

Tactic:
ofReal_neg,

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) (-↑2) = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    ↑(-1) ^ (k + 1) * ↑(2 * π) ^ (2 * k) / ↑2 / ↑↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
ofReal_neg,

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-↑1) ^ (k + 1) * ↑(2 * π) ^ (2 * k) / ↑2 / ↑↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I) =
    ↑(-1) ^ (k + 1) * ↑(2 * π) ^ (2 * k + 1) / ↑2 / ↑↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
ofReal_neg,

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / (2 * I) =
    (-↑1) ^ (k + 1) * ↑(2 * π) ^ (2 * k + 1) / ↑2 / ↑↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: 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
⊢ LSeriesSummable f s

Tactic:
by
  have h₁ : -s ≠ 0 := neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)
  have h₂ : (-s).re + r ≤ 0 := by
    rw [neg_re, neg_add_nonpos_iff]
    exact hs.le
  have h₃ (t : ℝ) (ht : t ∈ Set.Ici 1) : DifferentiableAt ℝ (fun x : ℝ ↦ ‖(x : ℂ) ^ (-s)‖) t :=
    have ht' : t ≠ 0 := (zero_lt_one.trans_le ht).ne'
    (differentiableAt_id.ofReal_cpow_const ht' h₁).norm ℝ <|
      (cpow_ne_zero_iff_of_exponent_ne_zero h₁).mpr <| ofReal_ne_zero.mpr ht'
  have h₄ : (deriv fun t : ℝ ↦ ‖(t : ℂ) ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1)) := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    rw [deriv_norm_ofReal_cpow _ ht, neg_re, neg_add']
  simp_rw [LSeriesSummable, funext (LSeries.term_def₀ hf s), mul_comm (f _)]
  refine summable_mul_of_bigO_atTop' (f := fun t ↦ (t : ℂ) ^ (-s))
    (g := fun t ↦ t ^ (-(s.re + 1) + r)) _ h₃ ?_ ?_ ?_ ?_
  · refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi
      (integrableOn_Ioi_deriv_norm_ofReal_cpow zero_lt_one ?_)).locallyIntegrableOn
    exact neg_re _ ▸ neg_nonpos.mpr <| hr.trans hs.le
  · refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right (by simp)
    exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop
  · refine h₄.isBigO.of_const_mul_right.mul_atTop_rpow_of_isBigO_rpow _ r _ ?_ le_rfl
    exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
      isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)
  · rwa [integrableAtFilter_rpow_atTop_iff, neg_add_lt_iff_lt_add, add_neg_cancel_right]

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

Goal state before:
pp: case zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

pp: case succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)

Tactic:
· simp [hf]

Goal state after:
case succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
⊢ False

Tactic:
have hq : 0 < (q.totient : ℝ)⁻¹ := inv_pos.mpr (mod_cast q.totient.pos_of_neZero)

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
⊢ False
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ HasSum (fun n ↦ 1 / ↑n ^ 4) (π ^ 4 / 90)

Tactic:
by
  convert! hasSum_zeta_nat two_ne_zero using 1
  simp only [Nat.reduceAdd, Nat.reduceMul, Nat.add_one_sub_one]
  rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]
  · simp [Nat.factorial]; ring
  · decide

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

Goal state before:
pp: f : ℕ → ℝ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ∑ k ∈ Icc 1 x✝, f k = ∑ k ∈ Icc 1 x✝, ‖↑(f k)‖

Tactic:
simp [abs_of_nonneg (hf _)]

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: 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
⊢ IsDiscrete R

Tactic:
rw [isNontrivial_iff_nontrivial_units] at h; push Not at h
    refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
    contrapose! hy
    have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
    exact Units.val_le_val.mpr this.le

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

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ≠ 0

Tactic:
rcases eq_zero_or_neZero b with hb | _

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0

case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | b) ≠ 0

pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
· rw [hb, zero_right]
    exact one_ne_zero

Goal state after:
case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b : ℕ
⊢ J(a ^ zero | b) = J(a | b) ^ zero

Tactic:
_root_.pow_zero,

Goal state after:
a : ℤ
e b : ℕ
⊢ J(1 | b) = J(a | b) ^ zero
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b : ℕ
⊢ J(1 | b) = J(a | b) ^ zero

Tactic:
_root_.pow_zero,

Goal state after:
a : ℤ
e b : ℕ
⊢ J(1 | b) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case zero
a : ℤ
b : ℕ
⊢ J(a | 1) = J(a | b) ^ 0

Tactic:
_root_.pow_zero,

Goal state after:
case zero
a : ℤ
b : ℕ
⊢ J(a | 1) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rcases eq_zero_or_neZero b with hb | _

Goal state after:
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
| χ ↑b.primeFactorsList.prod

Tactic:
cast_list_prod,

Goal state after:
a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
| χ (List.map Nat.cast b.primeFactorsList).prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
hb : Odd b
⊢ J(-a | b) = χ₄ ↑b * J(a | b)

Tactic:
neg_eq_neg_one_mul,

Goal state after:
a : ℤ
b : ℕ
hb : Odd b
⊢ J(-1 * a | b) = χ₄ ↑b * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ (↑2).gcd ↑b = 1

Tactic:
rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]

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

Goal state before:
pp: a : ℤ
b : ℕ
ha4 : a % 4 = 0
hb2 : b % 2 = 1
⊢ J(a / 4 | b) = J(a | b)

Tactic:
by
  obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4
  have : Int.gcd (2 : ℕ) b = 1 := by
    rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]
  rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left,
    (by decide : (4 : ℤ) = (2 : ℕ) ^ 2), jacobiSym.sq_one' this, one_mul]

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

Goal state before:
pp: a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
⊢ J(↑a | b) = -J(↑b | a)

Tactic:
let nop := @neg_one_pow_div_two_of_three_mod_four

Goal state after:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ J(↑a | b) = -J(↑b | a)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
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
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
· rw [fastJacobiSymAux.eq_jacobiSym, if_neg Bool.false_ne_true, mod_left a b,
      Int.natAbs_of_nonneg (a.emod_nonneg (mod_cast hb0))]
    · exact Nat.mod_two_ne_zero.mp hb2
    · exact lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr hb0) (Ne.symm hb1)

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ sMod p i < 2 ^ p - 1

Tactic:
rw [← sMod_mod]
  refine (Int.emod_lt_abs _ (mersenne_int_ne_zero p hp)).trans_eq ?_
  exact abs_of_nonneg (mersenne_int_pos hp).le

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑(2 ^ (p' + 2) - 1) * ↑k * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
mul_comm _ (k : X (q (p' + 2)))

Goal state after:
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∃ a, a • w = ![(w 1)⁻¹ * w 0, 1]

Tactic:
exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
k : K
⊢ g • ↑k = if ↑g 1 0 * k + ↑g 1 1 = 0 then ∞ else ↑((↑g 0 0 * k + ↑g 0 1) / (↑g 1 0 * k + ↑g 1 1))

Tactic:
by
  simp [Equiv.smul_def, mulVec_eq_sum, div_eq_inv_mul, mul_comm, Units.smul_def]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * (↑a₂ * ↑a₁ * ↑M) * (↑A₁.den)⁻¹) • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
mul_assoc _ _ (M : ℚ),

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ((↑A₂.den)⁻¹ * (↑a₂ * (↑a₁ * ↑M)) * (↑A₁.den)⁻¹) • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
x✝ : ℍ
⊢ (0 ∣[k] A) x✝ = 0 x✝

Tactic:
simp [privateSlash]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
this : Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
have _ : NeZero N := ⟨hN⟩

Goal state after:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
this : Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
x✝ : NeZero N
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : SL(2, ℤ)
f : ℍ → ℂ
c : α
τ : ℍ
⊢ ((c • f) ∣[k] A) τ = (c • f ∣[k] A) τ

Tactic:
simp [SL_slash_apply, Pi.smul_apply, smul_mul_assoc]

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
q : K
g : SL(2, A)
hg0 : ↑g 0 0 = IsFractionRing.num A q
hg1 : ↑g 1 0 = ↑(IsFractionRing.den A q)
⊢ (mapGL K) g • ∞ = ↑q

Tactic:
simp [hg0, hg1, smul_infty_eq_ite]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a⁻¹ * b ∈ Subgroup.comap (mapGL ℝ) 𝒢
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
refine Quotient.eq.mpr ⟨⟨_, hab⟩, ?_⟩

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a⁻¹ * b ∈ Subgroup.comap (mapGL ℝ) 𝒢
⊢ (fun m ↦ m • ⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩) ⟨(mapGL ℝ) (a⁻¹ * b), hab⟩ = ⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩
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
⊢ True ∧ z.re = -1 / 2

Tactic:
true_and

Goal state after:
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
⊢ z.re = -1 / 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
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
⊢ True ∧ z.re = 1 / 2

Tactic:
true_and

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
⊢ z.re = 1 / 2
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: x : ↥(divisorsAntidiagonal 1)
⊢ divisorsAntidiagonalFactors 1 x = (1, 1)

Tactic:
by
  have h := Nat.mem_divisorsAntidiagonal.mp x.2
  simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h
  simp [divisorsAntidiagonalFactors, h.1, h.2]

Goal state after:
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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ -S • T • ρ = ρ

Tactic:
← S_inv,

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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ S⁻¹ • T • ρ = ρ
Module: Mathlib.NumberTheory.Modular

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

Tactic:
← S_inv,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (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 • ρ
⊢ S⁻¹ • T⁻¹ • (1 +ᵥ ρ) = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: c : ℂ
z : ℍ
⊢ D (fun x ↦ c) z = 0 z

Tactic:
change (2 * π * I)⁻¹ * deriv (fun _ : ℂ ↦ c) (z : ℂ) = 0

Goal state after:
c : ℂ
z : ℍ
⊢ (2 * ↑π * I)⁻¹ * deriv (fun x ↦ c) ↑z = 0
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ serreDerivative (k₁ + k₂) (F * G) = serreDerivative k₁ F * G + F * serreDerivative k₂ G

Tactic:
by
  ext z
  simp [serreDerivative, normalizedDerivOfComplex_mul F G hF hG]
  ring_nf

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

Goal state before:
pp: k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ (↑((n • divIntMap ↑n ↑v) 0) * ↑z + ↑((n • divIntMap ↑n ↑v) 1)) ^ (-k) =
    (↑n ^ k)⁻¹ * (↑(divIntMap (↑n) (↑v) 0) * ↑z + ↑(divIntMap (↑n) (↑v) 1)) ^ (-k)

Tactic:
simp [← mul_inv, ← mul_zpow, mul_add, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ UpperHalfPlane.coe '' 𝒟ᵒ = {z | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}

Tactic:
ext x
  refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_lt_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
  rintro ⟨τ, hτ, rfl⟩
  exact ⟨τ.im_pos, one_lt_normSq_iff.mp hτ.1, hτ.2⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
x : ℍ
hx✝ : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
hx : 1 < ‖↑x‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
exact mem_closure_of_one_lt_norm hx hx'

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
h : 1 / 2 ≤ τ.im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) 1)) ↑τ‖ ≤ 1

Tactic:
simp only [map_one, denom_one, norm_one, le_refl]

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

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

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g