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

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
by
  rcases eq_or_ne p q with rfl | h
  · rfl
  · rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ 2 * a.succ ≤ a ^ b + 1

Tactic:
apply Nat.succ_le_succ

Goal state after:
a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ Nat.mul 2 a + 1 ≤ a ^ b
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
⊢ m * n - m - n ∈ {k | ∀ (m_1 n_1 : ℕ), m_1 • m + n_1 • n ≠ k}

Tactic:
intro a b h

Goal state after:
case left
m n : ℕ
cop : m.Coprime n
hm : 1 < m
hn : 1 < n
hmn : m + n ≤ m * n
a b : ℕ
h : a • m + b • n = m * n - m - n
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this : ¬p ∣ b
⊢ p ∣ b ^ (p - 1) - 1

Tactic:
have : p.Coprime b := Or.resolve_right (Nat.coprime_or_dvd_of_prime p_prime b) this

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
this✝ : ¬p ∣ b
this : p.Coprime b
⊢ p ∣ b ^ (p - 1) - 1
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : AddSubmonoid ℕ
⊢ s.FG

Tactic:
rw [← s.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg]

Goal state after:
s : AddSubmonoid ℕ
⊢ (AddSubmonoid.toNatSubmodule s).FG
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
⊢ ↑(harmonic n) ≤ 1 + Real.log ↑n

Tactic:
by
  by_cases hn0 : n = 0
  · simp [hn0]
  have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0
  simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]
  rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm,
    Nat.cast_one, inv_one]
  gcongr
  simp only [Finset.Icc_erase_left]
  calc ∑ d ∈ .Ico 2 (n + 1), (d : ℝ)⁻¹
    _ = ∑ d ∈ .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
    _ ≤ ∫ x in 2..↑(n + 1), (x - 1)⁻¹ := ?_
    _ = ∫ x in 1..n, x⁻¹ := ?_
    _ = Real.log ↑n := ?_
  · simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
  · exact @AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <|
      sub_inv_antitoneOn_Icc_right (by simp)
  · convert! intervalIntegral.integral_comp_sub_right _ 1
    · norm_num
    · simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]
  · convert! integral_inv _
    · rw [div_one]
    · simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg,
        and_true, not_le, zero_lt_one]

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

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ term n 1 = ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ 2

Tactic:
simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
val✝ : Fin n
⊢ (vecCons 0 x ∘ ⇑e) (Sum.inl val✝) = Sum.elim x 0 (Sum.inl val✝)

Tactic:
| =>

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
val✝ : Fin n
⊢ (vecCons 0 x ∘ ⇑e) (Sum.inl val✝) = Sum.elim x 0 (Sum.inl val✝)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
i : ℕ
h : i < 1
⊢ (vecCons 0 x ∘ ⇑e) (Sum.inr ⟨i, h⟩) = Sum.elim x 0 (Sum.inr ⟨i, h⟩)

Tactic:
| =>

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
i : ℕ
h : i < 1
⊢ (vecCons 0 x ∘ ⇑e) (Sum.inr ⟨i, h⟩) = Sum.elim x 0 (Sum.inr ⟨i, h⟩)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
he : vecCons 0 x ∘ ⇑e = Sum.elim x 0
⊢ mulHeight (vecCons 0 x) = mulHeight x

Tactic:
rw [← mulHeight_comp_equiv e, he, mulHeight_sumElim_zero_eq]

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
⊢ ∏ᶠ (w : FinitePlace K), w x = ↑|(Algebra.norm ℚ) x|⁻¹

Tactic:
rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
hb : b ∈ nonZeroDivisors (𝓞 K)
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹
Module: Mathlib.NumberTheory.Height.Basic

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

Tactic:
by
  simp only [mulHeight₁_eq_mulHeight]
  rw [show ![x * y, 1] = ![x, 1] * ![y, 1] by ext i; fin_cases i <;> simp]
  exact mulHeight_mul_le ![x, 1] ![y, 1]

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

Goal state before:
pp: case hfh
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
transitivity (n + 1) / (n + 1) ^ s

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (↑n + 1) / (↑n + 1) ^ s

s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)
Module: Mathlib.NumberTheory.Height.Basic

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

Tactic:
by
  rw [sub_eq_add_neg, ← mulHeight₁_neg y]
  exact mulHeight₁_add_le x (-y)

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

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

Tactic:
have := tendsto_riemannZeta_sub_one_div.add tendsto_Gamma_term_aux

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
ha : ↑n * x = ↑a
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r})) *
      (Submodule.toAddSubgroup (span {↑n, a})).index =
    n ^ finrank ℚ K

Tactic:
← RingOfIntegers.rank,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
a : 𝓞 K
ha' : ↑m * a = ↑n * r
ha : ↑n * x = ↑a
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r})) *
      (Submodule.toAddSubgroup (span {↑n, a})).index =
    n ^ finrank ℤ (𝓞 K)
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
a : AdjoinRoot f
⊢ h.adjoinRootAlgEquiv a = h.map ⋯.choose

Tactic:
rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n : ℕ
hn₁ : 0 < n
hn₂ : n < orderOf χ
⊢ gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)

Tactic:
induction n, hn₁ using Nat.le_induction with

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
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
have : (Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm

Goal state after:
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)))
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

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

Tactic:
by
  rw [sinZeta_two_mul_nat_add_one hk hx]
  congr 1
  have : (2 * k + 1)! = (2 * k + 1) * Complex.Gamma (2 * k + 1) := by
    rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
  simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]
  rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]
  ring

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑2 * ↑↑k ≠ -↑n

Tactic:
← Int.cast_mul,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(2 * ↑k) ≠ -↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑2 * ↑↑k + 1 ≠ -↑n

Tactic:
← Int.cast_mul,

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

Goal state before:
pp: case e_a
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ LSeries (fun n ↦ ↑(zeta n)) s = LSeries (⇑↑zeta) s

Tactic:
← natCoe_apply

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

Goal state before:
pp: case refine_2.inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
⊢ 1 ∈ {s | LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_ofPred_eq, one_re, le_refl,
        LFunction_ne_zero_of_one_le_re χ (.inl hχ), not_false_eq_true]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
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
x✝ : ℕ
⊢ ((fourier ↑x✝) ↑x - (fourier (-↑x✝)) ↑x) / (2 * I) = ↑(Real.sin (2 * π * ↑x✝ * x))

Tactic:
· rw [ofReal_sin, ofReal_mul, fourier_coe_apply, fourier_coe_apply, sin, ofReal_one, div_one,
        div_one, ofReal_mul, ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast,
        ofReal_natCast, ← div_div, div_I, div_mul_eq_mul_div₀, ← neg_div, ← neg_mul, neg_sub]
      congr 4
      · ring
      · ring

Goal state after:
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
⊢ False

Tactic:
have H₁ {x : ℝ} (hx : 1 < x) : ∑' n, residueClass a n / (n : ℝ) ^ x ≤ C := by
    refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key
    · rcases n.eq_zero_or_pos with rfl | hn
      · simp
      · refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
        conv_lhs => rw [← Real.rpow_one n]
        exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le
    · exact summable_real_of_abscissaOfAbsConv_lt <|
        (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| mod_cast hx

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
⊢ False
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
⊢ ∀ ⦃x₂ : ℕ → ℂ⦄, x₂ ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤} → LSeries f = LSeries x₂ → f = x₂

Tactic:
g

Goal state after:
f : ℕ → ℂ
hf : f ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}
g : ℕ → ℂ
⊢ g ∈ {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤} → LSeries f = LSeries g → f = g
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ (primitiveChar_to_Complex F).IsPrimitive

Tactic:
by
  refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
  let nn := (primitiveChar F ℂ <| ringChar_ne F).n
  exact (IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective

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

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n : ℕ
⊢ ∃ b, n ≤ b ∧ Prime b ∧ b ≡ a [MOD q]

Tactic:
obtain ⟨p, hn, hp, ha⟩ := forall_exists_prime_gt_and_modEq n hq h

Goal state after:
q a : ℕ
hq : q ≠ 0
h : a.Coprime q
n p : ℕ
hn : p > n
hp : Prime p
ha : p ≡ a [MOD q]
⊢ ∃ b, n ≤ b ∧ Prime b ∧ b ≡ a [MOD q]
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ∀ x ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯,
    x ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
intro _ ha'
        rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
        have : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
        exact quadraticChar_isQuadratic (ZMod p) a

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

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : Nat.Prime a_1 ∧ a_1 ∣ b), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ ↑p ∣ ↑b

Tactic:
Int.natCast_dvd_natCast,

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : Nat.Prime a_1 ∧ a_1 ∣ b), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ p ∣ b
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
rcases eq_or_ne b 0 with hb | hb

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

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

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : ↑a = ↑r.valMinAbs * ↑r.valMinAbs
⊢ False

Tactic:
← Int.cast_mul,

Goal state after:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : ↑a = ↑(r.valMinAbs * r.valMinAbs)
⊢ False
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ ↑↑z
b : K
z0 : 0 < (MonoidWithZeroHom.ofClass v) b
hb : (MonoidWithZeroHom.ofClass v) b = ↑↑z
⊢ IsOpen {w | v.restrict w ≤ v.restrict b}

Tactic:
refine Valued.isOpen_closedBall _ ?_

Goal state after:
case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ ↑↑z
b : K
z0 : 0 < (MonoidWithZeroHom.ofClass v) b
hb : (MonoidWithZeroHom.ofClass v) b = ↑↑z
⊢ v.restrict b ≠ 0
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
n : ℕ
y : ↥𝒪[K]
hy : y ∈ ↑(𝓂[K] ^ n)
hL : (fun x ↦ f n +ᵥ x) y ∈ ⋂ i, S i
⊢ f n ≡ (fun x ↦ f n +ᵥ x) y [SMOD 𝓂[K] ^ n • ⊤]

Tactic:
simpa [SModEq.sub_mem] using hy

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this✝ : NeZero n
this : ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
simpa [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, cyclotomic.monic n ℂ,
      Polynomial.cyclotomic.roots_eq_primitiveRoots_val]

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

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

Tactic:
by
  have hpdegC : (p.map (castRingHom ℂ)).degree ≠ 0 := by
    rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]
  obtain ⟨z, _⟩ := Splits.exists_eval_eq_zero (IsAlgClosed.splits <| p.map (castRingHom ℂ))
    hpdegC
  have hz₀ : z ≠ 0 := by
    contrapose hX
    simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero]
  have h_z_root : z ∈ p.aroots ℂ := by aesop
  obtain ⟨m, h_m_pos, h_prim⟩ := isPrimitiveRoot_of_mahlerMeasure_eq_one h hz₀ h_z_root
  use m, h_m_pos
  rw [cyclotomic_eq_minpoly h_prim h_m_pos]
  apply minpoly.isIntegrallyClosed_dvd <| isIntegral_of_mahlerMeasure_eq_one h h_z_root
  exact (mem_aroots.mp h_z_root).2

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 2) = ω ^ (2 ^ (p' + 1) * 2)

Tactic:
← Nat.pow_succ

Goal state after:
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 2) = ω ^ 2 ^ (p' + 1).succ
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ H = ⊤

Tactic:
← coe_eq_univ,

Goal state after:
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
a✝ : Nontrivial G
this : Dense ↑H ∨ ∃ a, zpowers a = H
hA : DiscreteTopology ↥H
h : Dense ↑H
⊢ ↑H = Set.univ
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
L : Type u_2
inst✝¹ : Field L
inst✝ : DecidableEq L
f : K →+* L
g : GL (Fin 2) K
c : K
⊢ OnePoint.map (⇑f) (g • ↑c) = (GeneralLinearGroup.map f) g • OnePoint.map ⇑f ↑c

Tactic:
| coe c =>

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

Goal state before:
pp: case coe
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
⊢ g • ↑c = ↑c ↔ ↑c = g.parabolicFixedPoint

Tactic:
| coe c =>

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

Goal state before:
pp: case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
⊢ g • ↑c ≠ ↑c

Tactic:
| coe c =>

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ -⇑f ∣[k] γ = -⇑f

Tactic:
slash_action_eqn f γ hγ

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ -⇑f = -⇑f
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ✝ : Subgroup (GL (Fin 2) ℝ)
k✝ : ℤ
inst✝¹ : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
f : (i : ι) → SlashInvariantForm Γ (k i)
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ (∏ i ∈ s, ⇑(f i)) ∣[m] A = ∏ i ∈ s, ⇑(f i)

Tactic:
simp [hm, prod_slash_sum_weights, -Matrix.GeneralLinearGroup.val_det_apply,
       Subgroup.HasDetPlusMinusOne.abs_det hA, SlashInvariantForm.slash_action_eqn (f _) A hA]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
⊢ f = 0

Tactic:
ext z
  have hf := slash_action_eqn'' f h_neg_one z
  rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf
  have h2 : (2 : ℂ) * f z = 0 := by linear_combination hf
  exact (mul_eq_zero.mp h2).resolve_left (by norm_num)

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
τ : ℍ
hh : h ≠ 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ cuspFunction h f (𝕢 h ↑τ) = f τ

Tactic:
by
  simpa [cuspFunction] using (Periodic.eq_cuspFunction hh hfper τ)

Goal state after: