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

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this : Fact (2 < p)
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1

Tactic:
have : Fact p.Prime := Fact.mk hp

Goal state after:
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
⊢ ∃ k, p = k * 2 ^ (n + 1) + 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case mp
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ n.ProbablePrime b → 1 ≡ b ^ (n - 1) [MOD n]

Tactic:
intro h₁
    apply Nat.modEq_of_dvd
    exact mod_cast h₁

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1

Tactic:
have : Fact p.Prime := Fact.mk hp

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
⊢ ∃ k, p = k * 2 ^ (n + 2) + 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ n.fermatNumber
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1

Tactic:
fermatNumber

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
hpdvd : p ∣ 2 ^ 2 ^ n + 1
this : Fact (Prime p)
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ p ∣ a.val ^ 2 ^ (n + 1) + 1
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 2 ≤ n + 1

Tactic:
linarith [hn]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime S.Y S.Z

Tactic:
by
  rw [← IsCoprime.pow_iff (m := 3) (n := 3) (by decide) (by decide),
    ← isCoprime_mul_unit_right_left S.u₂.isUnit, ← isCoprime_mul_unit_right_right S.u₃.isUnit,
    Y_u₂_spec, Z_u₃_spec]
  exact isCoprime_y_z S

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
have h_prod : (absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x})) : ℝ) =
      ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (absNorm (v.maxPowDividing (span {x})) : ℝ) :=
    ((Nat.castRingHom ℝ).toMonoidHom.comp absNorm.toMonoidHom).map_finprod_of_preimage_one
      (by simp) _

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ x.mulHeight

Tactic:
rw [← x.mk_rep, mulHeight_mk]
  exact Height.one_le_mulHeight _

Goal state after:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ x * χ⁻¹ (1 - x)

Tactic:
rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ (x / (1 - x))
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
g : S →+* T
hmap : ∀ (a : R), g ((algebraMap R S) a) = i a
hroot : g h.root = x
a : S
⊢ g a = (h.lift i x hx) a

Tactic:
rw [← h.map_repr a, Polynomial.as_sum_range_C_mul_X_pow (h.repr a)]
  simp [← h.algebraMap_apply, *]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ m ∉ Set.range Fin.val

Tactic:
rw [Set.mem_range, not_exists]

Goal state after:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ ∀ (x : Fin f.natDegree), ¬↑x = m
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ LFunction Φ s = LSeries (fun x ↦ Φ ↑x) s

Tactic:
LFunction,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
⊢ ↑N ^ (-s) * ∑ j, Φ j * hurwitzZeta (toAddCircle j) s = LSeries (fun x ↦ Φ ↑x) s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ LFunction χ x✝ = riemannZeta x✝

Tactic:
LFunction,

Goal state after:
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ ZMod.LFunction (⇑χ) x✝ = riemannZeta x✝
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
⊢ ofRealHom (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) =
    Polynomial.eval (ofRealHom x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
apply Polynomial.map_aeval_eq_aeval_map (by simp)

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

Goal state before:
pp: case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ ofRealHom (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (ofRealHom x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
apply Polynomial.map_aeval_eq_aeval_map (by simp)

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    ∑' (b : Nat.Primes),
      (3 * (-log (1 - 1 ↑↑b * ↑↑b ^ (-(1 + ↑x)))).re + 4 * (-log (1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y)))).re +
        (-log (1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y)))).re)

Tactic:
simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re,
    ofReal_re, ofReal_add, ofReal_one] using
      tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y

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

Goal state before:
pp: case e_a.inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ ↑(residueClass a n)) (↑x) n = ↑(term (fun n ↦ ↑(residueClass a n)) (↑x) n).re

Tactic:
· simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div,
        ofReal_re]

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

Goal state before:
pp: p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (p % 2 = 1)
a : ℕ
ha2✝ : a % 2 = 1
hap : ↑a ≠ 0
ha2 : ↑a = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) - ↑(∑ x ∈ Ico 1 (p / 2).succ, x * a / p) = 0

Tactic:
by
    simpa [add_left_comm, sub_eq_add_neg, ← mul_sum, mul_comm, ha2, Nat.cast_sum,
      add_neg_eq_iff_eq_add.symm, add_assoc] using
      Eq.symm (eisenstein_lemma_aux₁ p hap)

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

Goal state before:
pp: 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
⊢ -1 * J(↑b | a) = -J(↑b | a)

pp: case ha
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
⊢ Odd a

pp: case hb
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
⊢ Odd b

Tactic:
neg_one_mul

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(↑b | a) = -J(↑b | a)

case ha
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
⊢ Odd a

case hb
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
⊢ Odd b
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
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 : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
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 : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * ↑t ^ (-↑s - 1) - l * ↑t ^ (-↑s) = (S t - l * ↑t) * ↑t ^ (-↑s - 1)

Tactic:
rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ ht]

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

Goal state before:
pp: p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a

Tactic:
rw [legendreSym.to_jacobiSym, fastLegendreSym]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
⊢ sZMod p 0 = ↑(sMod p 0)

Tactic:
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]

Goal state after:
case zero
p : ℕ
⊢ 4 = 4
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ sZMod p (n✝ + 1) = ↑(sMod p (n✝ + 1))

Tactic:
push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *]

Goal state after:
case succ
p n✝ : ℕ
a✝ : sZMod p n✝ = ↑(sMod p n✝)
⊢ ↑(sMod p n✝) ^ 2 - 2 = ↑(sMod p n✝) ^ 2 - 2
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
← _root_.sq_sub_sq,

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ 1 ^ 2 - α ^ 2 = -2
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
obtain ⟨z, _⟩ := Splits.exists_eval_eq_zero (IsAlgClosed.splits <| p.map (castRingHom ℂ))
    hpdegC

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
⊢ ∃ n, 0 < n ∧ cyclotomic n ℤ ∣ p
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

Tactic:
have ht : t ≠ 0 := by rintro rfl; simp at hv

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case left
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).relIndex
      (Subgroup.map (mapGL ℝ) ⊤) ≠
    0

Tactic:
rw [← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]

Goal state after:
case left
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ) (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))

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

Goal state after:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ (σ A) (f (A • x)) * (σ A) (g (A • x)) * d ^ (k1 + k2 - 1) * (denom A ↑x ^ (-k1) * denom A ↑x ^ (-k2)) =
    d *
      ((σ A) (f (A • x)) * d ^ (k1 - 1) * denom A ↑x ^ (-k1) * ((σ A) (g (A • x)) * d ^ (k2 - 1) * denom A ↑x ^ (-k2)))

Tactic:
rw [h1]

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ (σ A) (f (A • x)) * (σ A) (g (A • x)) * (d * d ^ (k1 - 1) * d ^ (k2 - 1)) *
      (denom A ↑x ^ (-k1) * denom A ↑x ^ (-k2)) =
    d *
      ((σ A) (f (A • x)) * d ^ (k1 - 1) * denom A ↑x ^ (-k1) * ((σ A) (g (A • x)) * d ^ (k2 - 1) * denom A ↑x ^ (-k2)))
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
⊢ IsCusp c 𝒢

Tactic:
have hGH : 𝒢.relIndex ℋ ≠ 0 := 𝒢.relIndex_ne_zero

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : 𝒢.relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: case mp
f : ℍ → ℂ
k : ℤ
γ : SL(2, ℤ)
hc : IsCusp ((mapGL ℝ) γ • ∞) (mapGL ℝ).range
⊢ ((mapGL ℝ) γ • ∞).IsBoundedAt f k → ∃ γ_1, (mapGL ℝ) γ_1 • ∞ = (mapGL ℝ) γ • ∞ ∧ IsBoundedAtImInfty (f ∣[k] γ_1)

Tactic:
simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! fun hfc ↦ ⟨γ, rfl, hfc⟩

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
by
      rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
⊢ Tendsto (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop

Tactic:
let π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0

Goal state after:
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
⊢ Tendsto (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) cofinite atTop
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa [-upperRightHom_apply, ← AddChar.map_nsmul_eq_pow] using Subgroup.pow_mem _ h 2

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

Goal state before:
pp: case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa [-upperRightHom_apply, ← AddChar.map_nsmul_eq_pow] using Subgroup.pow_mem _ h 2

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.widthInfty ↔ IsCusp ∞ 𝒢

Tactic:
have : DiscreteTopology 𝒢.adjoinNegOne.strictPeriods := ‹_›
  rw [widthInfty, strictWidthInfty_pos_iff, (commensurable_adjoinNegOne_self 𝒢).isCusp_iff]

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

Goal state before:
pp: case refl
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
a : ModularForm Γ b.1
h2 : mcast ⋯ ⟨b.1, a⟩.snd ⋯ = b.snd
⊢ ⟨b.1, a⟩ = b

Tactic:
exact congr_arg _ h2

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t

Tactic:
obtain ⟨D, hD, hf_infinity⟩ := hf_infinity.exists_pos

Goal state after:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity✝ : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
hf_infinity : IsBigOWith D atImInfty f fun z ↦ z.im ^ t
⊢ ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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
this : g = -T ^ (-↑g 0 1)
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z

Tactic:
by intro z; conv_lhs => rw [this, SL_neg_smul]

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

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ v ᵥ* ↑γ ∈ gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

Tactic:
refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
  have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
  simp only [eq_intCast, Int.coe_castRingHom] at this
  simp_rw [Function.comp_def, this, hv.1]
  simp

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

Goal state before:
pp: case mp
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ qExpansion h f = 0 → f = 0

Tactic:
intro H
    ext z
    simp [← (hasSum_qExpansion hh hfper hfhol hfbdd z).tsum_eq, H]

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
⊢ ∫ (x : ℝ) in 0..h, ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
have hne : ‖(n : ℝ) ^ e‖ = n ^ e := Real.norm_of_nonneg (by positivity)

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
⊢ ∫ (x : ℝ) in 0..h, ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ IsZeroAtImInfty (⇑f ∣[k] γ)

Tactic:
show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ IsZeroAtImInfty ⇑f
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
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ

Tactic:
have hgeq : g = T ^ g 0 0 * S * T := by
    refine Subtype.ext ?_
    rw [coe_mul, coe_mul, coe_T_zpow, coe_S, coe_T, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]
    grind [g.property, det_fin_two]

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
⊢ (g = S * T ∨ g = T * S * T) ∧ z = ρ
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: h : ℝ
z : ℂ
⊢ logDeriv (𝕢 h) z = 2 * ↑π * I / ↑h

Tactic:
have : 𝕢 h = cexp ∘ ((2 * π * I / h) * ·) := by
    ext
    grind [Periodic.qParam]

Goal state after:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun x ↦ 2 * ↑π * I / ↑h * x
⊢ logDeriv (𝕢 h) z = 2 * ↑π * I / ↑h
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : ↑(k.toNat / 12) < (qExpansion 1 ⇑f).order
hk : 0 ≤ k
⊢ f = 0

Tactic:
· lift k to ℕ using hk
    exact sturm_bound_levelOne_nat (mod_cast h)

Goal state after: