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

Goal state before:
pp: ⊢ {n | Even n ∧ n.Abundant}.Infinite

Tactic:
rw [Set.infinite_iff_exists_gt]
  intro a
  have ha : Abundant 12 := by decide
  use (2 * (a + 1)) * 12
  grind [Abundant.mul_left ha (show 2 * (a + 1) ≠ 0 by grind)]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))

Tactic:
by
  rw [← quadraticChar_neg_one hF]
  have h := quadraticChar_card_card hF (ne_of_eq_of_ne (ringChar_zmod_n p) hp₁)
    (ne_of_eq_of_ne (ringChar_zmod_n p) hp₂.symm)
  rwa [card p] at h

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ (2 ^ (2 ^ n - 1) * 2 / 2) ≠ 1

Tactic:
Nat.mul_div_cancel _ two_pos,

Goal state after:
case hd
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
p : ℕ
hp1 : Prime p
hp2 : p ∣ 2 ^ 2 ^ n + 1 - 1
⊢ 3 ^ 2 ^ (2 ^ n - 1) ≠ 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - 1 - (b ^ 2 - 1) = b ^ (2 * p) - (1 + (b ^ 2 - 1))

Tactic:
by rw [Nat.sub_sub]

Goal state after:
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
a b : ℕ
h : a * m + b * n = m * n - (m + n)
⊢ (a + 1) * m + (b + 1) * n = m * n

Tactic:
zify [hmn] at 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)
⊢ (↑a + 1) * ↑m + (↑b + 1) * ↑n = ↑m * ↑n
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| ne_iff.mp hx
  suffices (fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).HasFiniteMulSupport by
    convert! this with v
    obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
    have : Nonempty ι := .intro i
    refine le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)
    rcases eq_or_ne (x j) 0 with h | h
    · rw [h, v.val.map_zero]
      exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩
    · exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl
  fun_prop (disch := grind)

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:
by
      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
x✝ : K
v : AbsoluteValue K ℝ
x : K
i : Fin 2
⊢ v (![x, 1] i) = ![v x, 1] i

Tactic:
fin_cases i <;> simp

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

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

Tactic:
rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]

Goal state after:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ((↑n + 1) ^ (-s + 1) - ↑n ^ (-s + 1)) / (-s + 1) -
      ↑n * (((↑n + 1) ^ (-(s + 1) + 1) - ↑n ^ (-(s + 1) + 1)) / (-(s + 1) + 1)) =
    1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
i : Fin (Nat.succ 0).succ
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: 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
y : ι' → K
hy : y ≠ 0
⊢ (mulHeight fun a ↦ x a.1 * y a.2) = mulHeight x * mulHeight y

Tactic:
by
  have hxy : (fun a : ι × ι' ↦ x a.1 * y a.2) ≠ 0 := by
    obtain ⟨i, hi⟩ := ne_iff.mp hx
    obtain ⟨j, hj⟩ := ne_iff.mp hy
    exact ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩
  rw [mulHeight_eq hx, mulHeight_eq hy, mulHeight_eq hxy, mul_mul_mul_comm, ← Multiset.prod_map_mul,
    ← finprod_mul_distrib
        (hasFiniteMulSupport_iSup_nonarchAbsVal hx) (hasFiniteMulSupport_iSup_nonarchAbsVal hy)]
  congr <;> ext1 v
  · exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v x y
  · exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v.val x y

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
i : Fin (Nat.succ 0).succ
⊢ ![x * y, 1] i = (![x, 1] * ![y, 1]) i

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ ↑x / (↑x + 1) ^ s) atTop (𝓝 0)

Tactic:
· apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
              (h := fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1))
      · rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
        refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
        exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)
      · intro n
        positivity
      · intro n
        dsimp only
        transitivity (n + 1) / (n + 1) ^ s
        · gcongr
          linarith
        · apply le_of_eq
          rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
          · norm_cast
          all_goals positivity

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ mulHeight₁ (∑ a ∈ s, x a) ≤ ↑(#s) ^ totalWeight K * ∏ a ∈ s, mulHeight₁ (x a)

Tactic:
simp only [mulHeight₁_eq, totalWeight]
  rw [prod_mul_distrib, ← prod_replicate, ← map_const, ← finprod_prod_comm _ _ (by fun_prop),
    ← prod_map_prod, ← mul_assoc, ← prod_map_mul]
  simp only [Function.const_apply]
  gcongr
  · exact finprod_nonneg fun _ ↦ by positivity
  · exact prod_map_nonneg fun _ h ↦ by positivity
  · exact prod_map_le_prod_map₀ _ _ (fun _ _ ↦ by positivity) fun _ _ ↦ max_abv_sum_one_le _ hs x
  · exact finprod_le_finprod (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
      fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x

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
⊢ mulHeight₁ (Finset.univ.sum ![x, y]) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)

Tactic:
mulHeight₁_sum_le Finset.univ_nonempty ![x, y]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ↑Finset.univ.card ^ totalWeight K * ∏ a, mulHeight₁ (![x, y] a) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)
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)
⊢ (mk K x.rep ⋯).logHeight = log (Height.mulHeight x.rep)

Tactic:
logHeight_mk,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ Height.logHeight x.rep = log (Height.mulHeight x.rep)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))

Tactic:
← prod_range_mul_prod_Ico _ (Nat.le_add_left k m),

Goal state after:
case refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ 1 < ((starRingEnd ℂ) z).re

Tactic:
by rwa [conj_re]

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
i : Fin (Nat.succ 0).succ
⊢ x✝ ↑(![a, ↑n] i) = x✝ (![↑a, ↑n] i)

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 i

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: ⊢ riemannZeta₀ 1 = ↑γ

Tactic:
by simp [riemannZeta₀]

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

Goal state before:
pp: case e'_2
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin (Nat.succ 0).succ
⊢ ![↑q.num, ↑↑q.den] i = (Int.cast ∘ ![q.num, ↑q.den]) i

Tactic:
fin_cases i <;> simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ Function.Injective Fin.val

Tactic:
exact Fin.val_injective

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

Goal state before:
pp: case e'_3.refine_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin 2
⊢ |![q.num, ↑q.den] i| ≤ max |q.num| ↑q.den

Tactic:
fin_cases i <;> simp

Goal state after:
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
⊢ ↑{J | J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)} ≃
    ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}

Tactic:
refine (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx')
    ?_ ?_).trans ?_
  · rwa [Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S), ← Ne]
  · by_contra h
    exact (show Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0 from
      Polynomial.map_monic_ne_zero (minpoly.monic hx')) (span_singleton_eq_bot.mp h)
  · refine (Ideal.normalizedFactorsEquivSpanNormalizedFactors ?_).symm
    exact Polynomial.map_monic_ne_zero (minpoly.monic hx')

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - ↑p ^ (-s)

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
    fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
by
  rcases χ.even_or_odd with hχ | hχ <;>
  rw [hχ.gammaFactor_def]
  · exact LFunction_eq_completed_div_gammaFactor_even hχ.to_fun _ (h.imp_right χ.map_zero')
  · apply LFunction_eq_completed_div_gammaFactor_odd hχ.to_fun

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

Goal state before:
pp: case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 0 * ZMod.completedLFunction (𝓕 ⇑χ) s

pp: case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : ¬χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
· rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : ¬χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a.e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑(↑n + 1) ^ ↑x = (↑(↑n + 1)⁻¹ ^ ↑x)⁻¹

Tactic:
rw [← cpow_neg, show (-x : ℂ) = (-1 : ℝ) * x by simp, cpow_mul_ofReal_nonneg Hn,
    Real.rpow_neg_one, inv_inv]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ (fun x ↦ LFunctionTrivChar N (1 + ↑x)) =O[𝓝[>] 0] fun x ↦ 1 / ↑x

Tactic:
by
  have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by
    have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
    exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ
  exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Tactic:
have : ContinuousOn (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) (Set.Icc 1 2) :=
    continuous_re.continuousOn.comp (t := Set.univ) (continuousOn_LFunctionResidueClassAux a)
      (fun ⦃x⦄ a ↦ trivial) |>.comp continuous_ofReal.continuousOn fun x hx ↦ by
        simpa only [Set.mem_ofPred_eq, ofReal_re] using hx.1

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ᶠ (p : ℕ) in atTop, Prime p ∧ p ≡ a [MOD q]

Tactic:
rw [frequently_atTop]
  intro n
  obtain ⟨p, hn, hp, ha⟩ := forall_exists_prime_gt_and_modEq n hq h
  exact ⟨p, hn.le, hp, ha⟩

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

Goal state before:
pp: a : ℤ
b : ℕ
⊢ {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom)

Tactic:
Set.pair_comm

Goal state after:
a : ℤ
b : ℕ
⊢ {0, -1, 1} = ↑(MonoidHom.mrange ↑SignType.castHom)
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 : ¬Nontrivial (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R

Tactic:
push Not at h

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Subsingleton (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)

Tactic:
gauss_lemma hp ha0',

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑↑a * ↑x).val}) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J((n :: l').prod | n✝) = (List.map (fun a ↦ J(a | n✝)) (n :: l')).prod

Tactic:
rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

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

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

Tactic:
jacobiSym.mul_left,

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ J(a | b) = J(4 | b) * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = J(2 * a | b)

Tactic:
jacobiSym.mul_left,

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = J(2 | b) * J(a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x : ↥𝒪[K]
ht' : ∃ i ∈ t, dist x i < ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t

Tactic:
obtain ⟨y, hy, hy'⟩ := ht'

Goal state after:
case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ Set.univ →
    Quot.mk (⇑(Submodule.quotientRel (IsLocalRing.maximalIdeal ↥𝒪[K]))) x ∈ ⇑(IsLocalRing.residue ↥𝒪[K]) '' t
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
⊢ (Set.Icc x y).Finite

Tactic:
have H : (Set.Icc y⁻¹ 1).Finite := this _

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ (Set.Icc x y).Finite
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz)) }
y : ↥K := ⟨z, ⋯⟩
⊢ ∃ n, ∃ (_ : 0 < n), y ^ n = 1

Tactic:
refine NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
⊢ φ y ∈ p.aroots ℂ
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
⊢ ((f * g) ∣[k1 + k2] A) x = (|↑(Matrix.GeneralLinearGroup.det A)| • (f ∣[k1] A * g ∣[k2] A)) x

Tactic:
simp only [slash_apply, Pi.mul_apply, Pi.smul_apply, real_smul, map_mul, neg_add,
    zpow_add₀ (denom_ne_zero _ x)]

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