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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
⊢ mulHeight (c • x) = mulHeight x

Tactic:
have hcx : c • x ≠ 0 := by simp [hc, hx]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
this : Nonempty ι
hcx : c • x ≠ 0
⊢ mulHeight (c • x) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case h₁
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((x ∘ f) i)) archAbsVal).prod ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod

pp: case h₂
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
· exact Multiset.prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _)
      fun v _ ↦ H v

Goal state after:
case h₂
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
this : Nonempty ι
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((x ∘ f) i) ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
⊢ mulHeight (Sum.elim x 0) = mulHeight x

Tactic:
have : Nonempty ι := .intro i

Goal state after:
case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight (Sum.elim x 0) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
⊢ mulHeight x = 1

Tactic:
have : Nonempty ι := .intro i

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ mulHeight x = 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
hy : y ≠ 0
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]

Tactic:
rw [mulHeight₁_eq_mulHeight, ← mulHeight_smul_eq_mulHeight _ hy]
    simp [mul_div_cancel₀ x hy]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x * y)) ≤ log (mulHeight₁ x * mulHeight₁ y)

Tactic:
exact log_le_log (by positivity) <| mulHeight₁_mul_le ..

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ (fun z ↦ f z - f 1) =o[𝓝[≠] 1] fun z ↦ (z - 1)⁻¹

Tactic:
refine Asymptotics.isLittleO_of_tendsto' ?_ ?_

Goal state after:
case refine_2.refine_1
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0

case refine_2.refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2 / Gammaℝ 1))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))

Tactic:
rw [Gammaℝ_one, div_one] at this

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.toList.length = archAbsVal.toList.length • 1

Tactic:
Multiset.length_toList,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = archAbsVal.card • 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
      push_cast]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ (↑(absNorm v.maximalIdeal.asIdeal ^ ⨅ i, multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)

Tactic:
map_iInf_of_monotone (fun _ ↦ multiplicity ..) (pow_right_monotone <| by lia),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ (↑(⨅ i, absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)
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
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ↑(#(univ \ {0, 1})) = ↑(Fintype.card F) - 2

Tactic:
rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
      Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ ⨆ i, (↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)

Tactic:
refine iSup_congr fun i ↦ ?_

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
i : ι
⊢ (↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = v ↑(x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e'_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ -(s - 1)⁻¹ ^ 2 + deriv riemannZeta₀ s = deriv (fun s ↦ (s - 1)⁻¹ + riemannZeta₀ s) s

Tactic:
rw [deriv_fun_add (by fun_prop) (by fun_prop), deriv_fun_inv'' (by fun_prop) (by exact this)]
    simp [field]

Goal state after:
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 : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ g %ₘ f - g

Tactic:
modByMonic_eq_sub_mul_div,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ g - f * (g /ₘ f) - g
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ Irreducible y

Tactic:
exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])

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

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

Tactic:
sinZeta_two_mul_nat_add_one' hk hx,

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

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0

Tactic:
bernoulliFourierCoeff,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun k x)) 0 = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e'_2
⊢ riemannZeta ↑2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

Tactic:
zeta_nat_eq_tsum_of_gt_one one_lt_two

Goal state after:
case e'_2
⊢ ∑' (n : ℕ), 1 / ↑n ^ 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case refine_2.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ ∑ j, Φ j = 0 → DifferentiableAt ℂ (fun x ↦ (∑ j, Φ j) / (1 - x)) s

Tactic:
exact fun h ↦ by simp only [h, zero_div, differentiableAt_const]

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f + g) s n = term f s n + term g s n

Tactic:
simp [term_add]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (-f) s

Tactic:
by
  simpa [LSeriesSummable, term_neg] using! Summable.neg hf

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

Goal state before:
pp: case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (↑↑p)⁻¹ ≤ 1 - 2⁻¹

Tactic:
show (1 : ℝ) - 2⁻¹ = 2⁻¹ by norm_num,

Goal state after:
case hbc
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ (↑↑p)⁻¹ ≤ 2⁻¹
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x

Tactic:
· rw [one_div, inv_pow, pow_succ _ 3, ← mul_assoc,
        inv_mul_cancel₀ <| pow_ne_zero 3 (ofReal_ne_zero.mpr h), one_mul, mul_one]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ AddChar F ℂ

Tactic:
by
  letI ch := primitiveChar F ℂ <| by exact ringChar_ne F
  refine MonoidHom.compAddChar ?_ ch.char
  exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
⊢ (valuation K) (r ^ 2) < 1

Tactic:
by simpa [pow_two]

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

Goal state before:
pp: case ind.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : a = 1
⊢ (if flip = true then -1 else 1) = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rename_i ha1

Goal state after:
case ind.isFalse.isFalse.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : a = 1
⊢ (if flip = true then -1 else 1) = if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
h✝ : ¬a = 1
⊢ (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rename_i ha1

Goal state after:
case ind.isFalse.isFalse.isFalse
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
⊢ (if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
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) • of fun i j ↦ (y - 1) i j / (↑a₁ * ↑a₂ * ↑M)) i j

Tactic:
simp_rw [Matrix.smul_apply, Matrix.of_apply, nsmul_eq_mul, Nat.cast_mul]

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
⊢ (y - 1) i j = ↑a₁ * ↑a₂ * ↑M * ((y - 1) i j / (↑a₁ * ↑a₂ * ↑M))
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 * k * A₂.num)).map Int.cast =
    (↑A₁.den)⁻¹ • A₁.num.map Int.cast * (a₁ * a₂ * M) • k.map Int.cast * (↑A₂.den)⁻¹ • A₂.num.map Int.cast

Tactic:
simp only [Matrix.smul_mul, Matrix.mul_smul, Matrix.map_smul (Int.cast : ℤ → ℚ) M (by simp),
      Matrix.map_mul_intCast]

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.Cusps

Goal state before:
pp: case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
· rintro ⟨g, rfl⟩
    refine ⟨mapGL ℚ g • ∞, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
       ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

Goal state after:
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
τ : ℍ
this : ‖𝕢 h ↑τ‖ < 1
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) • 𝕢 h ↑τ ^ m) (f τ)

Tactic:
simpa [eq_cuspFunction τ hh.ne' hfper] using
    hasSum_qExpansion_of_norm_lt hh hfper hfhol hfbdd this

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
⊢ (T⁻¹ • z).im = z.im

Tactic:
by simpa using im_T_zpow_smul z (-1)

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

Goal state before:
pp: r : ℕ
a : Fin 2 → ZMod 1
⊢ gammaSet 1 r a = {v | (v 0).gcd (v 1) = r}

Tactic:
simp [gammaSet, Subsingleton.eq_zero (α := Fin 2 → ZMod 1)]

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

Goal state before:
pp: r : ℕ
v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r

Tactic:
simp [gammaSet, Subsingleton.eq_zero (α := Fin 2 → ZMod 1)]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hf : IsZeroAtImInfty f
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
⊢ f =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)

Tactic:
by
  simpa [hf.valueAtInfty_eq_zero] using exp_decay_sub_atImInfty hh hfper hfhol hfbdd

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

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ (𝓝[≠] 0).limUnder ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
exact (Periodic.tendsto_nhds_zero hfcts).mul (Periodic.tendsto_nhds_zero hgcts) |>.limUnder_eq

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

Goal state before:
pp: h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
h2 : iteratedDeriv m 1 0 = if m = 0 then 1 else 0
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1

Tactic:
simp +contextual [qExpansion_coeff, h1, h2]

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)‖
⊢ ‖(PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)‖ ≤ 1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
ModularFormClass.qExpansion_coeff_eq_intervalIntegral (t := 1 / n) f hh hΓ _ (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)‖
⊢ ‖1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑(1 / ↑n) * I) ^ n * f { coe := ↑u + ↑(1 / ↑n) * I, coe_im_pos := ⋯ }‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑g 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ ⌊1 + 1 / 2⌋ = 1

Tactic:
Int.floor_eq_iff

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑g 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ ↑1 ≤ 1 + 1 / 2 ∧ 1 + 1 / 2 < ↑1 + 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
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
⊢ √1 = 1

Tactic:
Real.sqrt_one

Goal state after:
case hnorm
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
⊢ 1 = 1
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ D (F * G) z = (D F * G + F * D G) z

Tactic:
simp only [normalizedDerivOfComplex, Pi.add_apply, Pi.mul_apply]

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((F * G) ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z * G z + F z * ((2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N a : ℕ
⊢ 0 < ((↑a + 1) * ↑z).im

Tactic:
simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2

Goal state after: