mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
⊢ (algebraMap (𝓞 K) K) ↑η ^ 2 + (algebraMap (𝓞 K) K) ↑η + 1 - 3 * (algebraMap (𝓞 K) K) ↑η =
    0 - 3 * (algebraMap (𝓞 K) K) ↑η

Tactic:
by simpa using hζ.isRoot_cyclotomic (by decide)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : (𝓞 K)ˣ
⊢ x✝ ∈ torsion K ↔ x✝ ∈ (AddMonoidHom.toMultiplicativeRight (logEmbedding K)).ker

Tactic:
rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicativeRight_apply_apply, ofAdd_eq_one,
          ← logEmbedding_eq_zero_iff]

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : Prime n
⊢ (n ^ m).Deficient

Tactic:
by
  rcases Nat.eq_zero_or_pos m with (rfl | _)
  · simpa using deficient_one
  · rw [Deficient, properDivisors_prime_pow h]
    calc
      ∑ x ∈ Finset.map ⟨(n ^ ·), Nat.pow_right_injective h.two_le⟩ (range m), x
        = ∑ i ∈ range m, n ^ i := by simp
      _ = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
      _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1)
      _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)

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

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : Fintype F
hF : ¬ringChar F = 2
⊢ IsSquare 2 ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5

Tactic:
· have h := FiniteField.odd_card_of_char_ne_two hF
    rw [← quadraticChar_one_iff_isSquare (Ring.two_ne_zero hF), quadraticChar_two hF,
      χ₈_nat_eq_if_mod_eight]
    lia

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ λ ∣ ↑c

pp: case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ↑a ↑b

pp: case refine_5
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ ↑a ^ 3 + ↑b ^ 3 = ↑1 * ↑c ^ 3

Tactic:
· exact dvd_trans hζ.toInteger_sub_one_dvd_prime' ⟨x, by simp [hx]⟩

Goal state after:
case refine_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ IsCoprime ↑a ↑b

case refine_5
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
H : FermatLastTheoremForThreeGen hζ
a b c : ℤ
hc : c ≠ 0
ha : ¬3 ∣ a
hb : ¬3 ∣ b
x✝ : 3 ∣ c
hcoprime : IsCoprime a b
h : a ^ 3 + b ^ 3 = c ^ 3
x : ℤ
hx : c = 3 * x
⊢ ↑a ^ 3 + ↑b ^ 3 = ↑1 * ↑c ^ 3
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n + 1) * (2 ^ 2 ^ n - 1) = 2 ^ 2 ^ (n + 1) + 1 - 2

Tactic:
← sq_sub_sq

Goal state after:
case succ
n : ℕ
hn : ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2
⊢ (2 ^ 2 ^ n) ^ 2 - 1 ^ 2 = 2 ^ 2 ^ (n + 1) + 1 - 2
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)
⊢ 2 ∣ b ^ p + b

Tactic:
← even_iff_two_dvd,

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)
⊢ Even (b ^ p + b)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: m n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
⊢ s.FG

Tactic:
refine ⟨t ∪ {m ∈ Finset.range n | m ∈ s}, (Submodule.span_le.mpr ?_).antisymm fun m hm ↦ ?_⟩

Goal state after:
case refine_1
m n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
⊢ ↑(t ∪ {m ∈ Finset.range n | m ∈ s}) ⊆ ↑s

case refine_2
m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
⊢ m ∈ Submodule.span ℕ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
x✝ : ∃ n, FrobeniusNumber n s
n : ℕ
hn : FrobeniusNumber n s
⊢ setGcd s = 1 ∧ 1 ∉ s

Tactic:
rw [frobeniusNumber_iff] at hn

Goal state after:
s : Set ℕ
x✝ : ∃ n, FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
⊢ setGcd s = 1 ∧ 1 ∉ s
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
x✝ : ∃ n, FrobeniusNumber n s
n : ℕ
hn : n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
⊢ setGcd s = 1 ∧ 1 ∉ s

Tactic:
exact ⟨dvd_one.mp <| Nat.dvd_add_iff_right (setGcd_dvd_of_mem_closure (hn.2 (n + 1)
      (by lia))) (n := 1) |>.mpr (setGcd_dvd_of_mem_closure (hn.2 (n + 2) (by lia))),
      fun h ↦ hn.1 <| AddSubmonoid.closure_mono (Set.singleton_subset_iff.mpr h)
        (addSubmonoidClosure_one.ge ⟨⟩)⟩

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

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 1 < padicNorm 2 (harmonic n)

Tactic:
rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',
      padicValRat_two_harmonic, neg_neg, zpow_natCast]

Goal state after:
n : ℕ
h : 2 ≤ n
⊢ 1 < ↑2 ^ Nat.log 2 n
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
⊢ S.a + S.b + (S.a + ↑η * S.b) * ↑η + S.z * λ * ↑η ^ 2 = 0

Tactic:
mul_comm S.z,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.a + S.b + (S.a + ↑η * S.b) * ↑η + λ * S.z * ↑η ^ 2 = 0
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
i : ι
hi : x i ≠ 0 i
this : Nonempty ι
⊢ Sum.elim x 0 (Sum.inl i) ≠ 0 (Sum.inl i)

Tactic:
simpa using hi

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ↑Finset.univ.card * ((⨆ ji, v (A ji)) * ⨆ i, v (x i)) ≤ ↑(Nat.card ι) * ((⨆ ji, v (A ji)) * ⨆ i, v (x i))

Tactic:
Finset.card_univ,

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
⊢ ↑(Fintype.card ι) * ((⨆ ji, v (A ji)) * ⨆ i, v (x i)) ≤ ↑(Nat.card ι) * ((⨆ ji, v (A ji)) * ⨆ i, v (x i))
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
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
⊢ mulHeight x = mulHeight fun i ↦ x ↑i

Tactic:
have hx : x ∘ e = Sum.elim (fun i : x.support ↦ x i.val) 0 := by
    ext1 i
    simp only [comp_apply]
    cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
hx : x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0
⊢ mulHeight x = mulHeight fun i ↦ x ↑i
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (Module.finrank ℚ K - 1)
⊢ ↑n ≤ mulHeight₁ x

Tactic:
← totalWeight_eq_finrank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑n ≤ mulHeight₁ x
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) =O[𝓝 1] fun x ↦ x - 1

Tactic:
suffices DifferentiableAt ℝ (fun (s : ℝ) ↦ (riemannZeta₁ s).re.log) 1 by
    simpa using this.isBigO_sub

Goal state after:
⊢ DifferentiableAt ℝ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (fun s ↦ (riemannZeta₁ s)⁻¹ - 1) =O[𝓝 1] fun x ↦ x - 1
⊢ (fun s ↦ (s - 1) * ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] fun s ↦ (s - 1) ^ 2

Tactic:
simpa [pow_two] using (isBigO_refl ..).mul this

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
⊢ {x | ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B}.Finite

Tactic:
set B' := B / n ^ (totalWeight K - 1)
  suffices Set.BijOn ((↑) : 𝓞 K → K) {x | ∀ (v : InfinitePlace K), v x ≤ B'}
      {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'} from
    this.finite_iff_finite.mpr (Embeddings.finite_of_norm_le K ℂ B') |>.subset
      fun _ _ ↦ by grind [infinitePlace_apply_le_of_prod_le hn B]
  refine .mk (fun x hx ↦ ?_) (fun _ _ _ _ ↦ RingOfIntegers.ext) fun a ha ↦ ?_ <;>
    simp only [Set.mem_image, Set.mem_ofPred_eq] at *
  · exact ⟨x.isIntegral_coe, fun φ ↦ hx <| .mk φ⟩
  · rw [← mem_integralClosure_iff ℤ K] at ha
    exact ⟨⟨a, ha.1⟩, fun v ↦ v.norm_embedding_eq a ▸ ha.2 v.embedding, rfl⟩

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 /ₘ f) - g

Tactic:
sub_right_comm,

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 - g - f * (g /ₘ f)
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
hdeg : 1 < f.natDegree
⊢ h.basis ⟨1, hdeg⟩ = h.root

Tactic:
rw [h.basis_apply, Fin.val_mk, pow_one]

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

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

Tactic:
refine Filter.EventuallyEq.deriv_eq ?_
  have h : {z | 1 < z.re} ∈ nhds s :=
    (isOpen_lt continuous_const continuous_re).mem_nhds hs
  filter_upwards [h] with z hz
  exact LFunction_eq_LSeries χ hz

Goal state after:
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:
rw [LFunction, LSeries, mul_sum, Nat.sumByResidueClasses (LSeriesSummable_of_one_lt_re Φ hs) N]
  congr 1 with j
  have : (j.val / N : ℝ) ∈ Set.Icc 0 1 := mem_Icc.mpr ⟨by positivity,
    (div_le_one (Nat.cast_pos.mpr <| NeZero.pos _)).mpr <| Nat.cast_le.mpr (val_lt j).le⟩
  rw [toAddCircle_apply, ← (hasSum_hurwitzZeta_of_one_lt_re this hs).tsum_eq, ← mul_assoc,
    ← tsum_mul_left]
  congr 1 with m
  -- The following manipulation is slightly delicate because `(x * y) ^ s = x ^ s * y ^ s` is
  -- false for general complex `x`, `y`, but it is true if `x` and `y` are non-negative reals, so
  -- we have to carefully juggle coercions `ℕ → ℝ → ℂ`.
  calc N ^ (-s) * Φ j * (1 / (m + (j.val / N : ℝ)) ^ s)
  _ = Φ j * (N ^ (-s) * (1 / (m + (j.val / N : ℝ)) ^ s)) := by
    rw [← mul_assoc, mul_comm _ (Φ _)]
  _ = Φ j * (1 / (N : ℝ) ^ s * (1 / ((j.val + N * m) / N : ℝ) ^ s)) := by
    simp only [cpow_neg, ← one_div, ofReal_div, ofReal_natCast, add_comm, add_div, ofReal_add,
      ofReal_mul, mul_div_cancel_left₀ (m : ℂ) (Nat.cast_ne_zero.mpr (NeZero.ne N))]
  _ = Φ j / ((N : ℝ) * ((j.val + N * m) / N : ℝ)) ^ s := by -- this is the delicate step!
    rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg] <;> positivity
  _ = Φ j / (N * (j.val + N * m) / N) ^ s := by
    simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]
  _ = Φ j / (j.val + N * m) ^ s := by
    rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]
  _ = Φ ↑(j.val + N * m) / (↑(j.val + N * m)) ^ s := by
    simp only [Nat.cast_add, Nat.cast_mul, natCast_zmod_val, natCast_self, zero_mul, add_zero]
  _ = LSeries.term (Φ ·) s (j.val + N * m) := by
    rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs)]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
have H : deriv (LFunctionTrivChar₁ n) s =
      deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s := by
    refine eventuallyEq_iff_exists_mem.mpr ?_ |>.deriv_eq
    exact ⟨_, isOpen_ne.mem_nhds hs, fun _ hw ↦ Function.update_of_ne (Set.mem_ofPred.mp hw) ..⟩
  rw [H, deriv_fun_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const,
    deriv_id'', one_mul, add_comm]

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

Goal state before:
pp: case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x, Φ x * hurwitzZetaEven (toAddCircle x) s + ∑ x, Φ x * hurwitzZetaOdd (toAddCircle x) s =
    ∑ j, Φ j * hurwitzZetaOdd (toAddCircle j) s

Tactic:
simp only [add_eq_right, ← neg_eq_self, ← sum_neg_distrib]

Goal state after:
case e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ ∑ x, -(Φ x * hurwitzZetaEven (toAddCircle x) s) = ∑ x, Φ x * hurwitzZetaEven (toAddCircle x) s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
⊢ LFunction χ (1 + I * ↑t) ≠ 0

Tactic:
by
  intro Hz
  have hz₁ : t ≠ 0 ∨ χ ≠ 1 := by
    refine h.symm.imp_right (fun h H ↦ ?_)
    simp only [H, one_pow, ne_eq, not_true_eq_false] at h
  have hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1 :=
    h.symm.imp_left <| mul_ne_zero two_ne_zero
  have help (x : ℝ) : ((1 / x) ^ 3 * x ^ 4 * 1 : ℂ) = x := by
    rcases eq_or_ne x 0 with rfl | h
    · rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]
    · 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]
  -- put together the various `IsBigO` statements and `norm_LFunction_product_ge_one`
  -- to derive a contradiction
  have H₀ : (fun _ : ℝ ↦ (1 : ℝ)) =O[𝓝[>] 0]
      fun x ↦ LFunctionTrivChar N (1 + x) ^ 3 * LFunction χ (1 + x + I * t) ^ 4 *
                   LFunction (χ ^ 2) (1 + x + 2 * I * t) :=
    IsBigO.of_bound' <| eventually_nhdsWithin_of_forall
      fun _ hx ↦ (norm_one (α := ℝ)).symm ▸ (χ.norm_LFunction_product_ge_one hx t).le
  have H := (LFunctionTrivChar_isBigO_near_one_horizontal (N := N)).pow 3 |>.mul <|
    (χ.LFunction_isBigO_horizontal_of_eq_zero hz₁ Hz).pow 4 |>.mul <|
    LFunction_isBigO_horizontal _ hz₂
  simp only [ofReal_mul, ofReal_ofNat, mul_left_comm I, ← mul_assoc, help] at H
  -- go via absolute value to translate into a statement over `ℝ`
  replace H := (H₀.trans H).norm_right
  simp only [norm_real] at H
  exact isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
    H.of_norm_right.trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

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
H₁ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
⊢ False

Tactic:
obtain ⟨C', hC'⟩ := LSeries_residueClass_lower_bound ha

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

Goal state before:
pp: ⊢ IsClosed riemannZetaZeros

Tactic:
by
  simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).1

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

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

Tactic:
· rw [← min_sub_sub_right, add_sub_cancel_left, ← lt_div_iff₀' h₀]
        exact (min_le_left ..).trans_lt <| div_lt_self (div_pos hq h₀) one_lt_two

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)

Tactic:
simpa using! hlim

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

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

Tactic:
rw [← neZero_iff] at hb

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

Goal state before:
pp: case ind.isFalse.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
hba : ¬b % a = 0
⊢ fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rw [IH (b % a) (b.mod_lt ha0) (Nat.mod_two_ne_zero.mp ha2) (lt_of_le_of_ne ha0 (Ne.symm ha1))]

Goal state after:
case ind.isFalse.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
hba : ¬b % a = 0
⊢ (if (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) = true then -J(↑(b % a) | a) else J(↑(b % a) | a)) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.specialize_2
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
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
⊢ w ∈ ↑𝒪[K] → w ∈ ⋃ i, U i

Tactic:
simp only [integer, SetLike.mem_coe, Valuation.mem_integer_iff, Set.mem_iUnion, U]

Goal state after:
case inr.specialize_2
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
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
⊢ v w ≤ 1 → ∃ i, w ∈ if v i ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v i}
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case h
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
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := ⋯
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : v w ≤ 1
⊢ w ∈ if v (if v w ≤ ↑↑z then a else w) ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w_1 | v w_1 = v (if v w ≤ ↑↑z then a else w)}

Tactic:
split_ifs <;>
    simp_all

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ y * x * a * y = y * (x * a) * y

Tactic:
rw [mul_assoc y x a]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ IsLocalRing.maximalIdeal ↥v.integer ≠ ⊥

Tactic:
by
  simp_rw [ne_eq, eq_bot_iff, v.isNontrivial_iff_exists_lt_one, SetLike.le_def, Ideal.mem_bot,
    not_forall, exists_prop, IsLocalRing.notMem_maximalIdeal.not_right,
    Valuation.Integer.not_isUnit_iff_valuation_lt_one]
  exact ⟨fun ⟨x, hx0, hx1⟩ ↦ ⟨⟨x, hx1.le⟩, by simp [Subtype.ext_iff, *]⟩,
  fun ⟨x, hx1, hx0⟩ ↦ ⟨x, by simp [*]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case refine_2
p' : ℕ
⊢ ¬(mersenne (p' + 2)).minFac = 2

Tactic:
minFac_eq_two_iff,

Goal state after:
case refine_2
p' : ℕ
⊢ ¬2 ∣ mersenne (p' + 2)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst✝² : Monoid G
inst✝¹ : AddCommGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
⊢ (∑ i ∈ s, a i) ∣[k] g = ∑ i ∈ s, a i ∣[k] g

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]

Goal state after: