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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
k : ι
⊢ ↑(abv ((bS.repr a) k)) < y

Tactic:
exact hy k

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
lt : abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b)
⊢ c = 0

Tactic:
contrapose! lt with c_ne_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : EuclideanDomain R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
abv : AbsoluteValue R ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
c : S
hc : c ∈ ↑I
c_ne_zero : c ≠ 0
⊢ abv ((Algebra.norm R) b) ≤ abv ((Algebra.norm R) c)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
⊢ False

Tactic:
obtain ⟨j₀, j₁, j_ne, approx⟩ := exists_approx_polynomial hb hε
      (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j_ne : j₀ ≠ j₁
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₁ % b -
          Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₀ % b)) <
    cardPowDegree b • ε
⊢ False
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1

Tactic:
· have := x.norm_sub_zmodRepr_lt_one
    constructor <;> intro h <;> rw [← h] at this ⊢
    · exact norm_eq_of_norm_sub_lt_right this
    · exact (norm_eq_of_norm_sub_lt_left this).symm

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ (lift f_compat) r - g r ∈ Ideal.span {↑p ^ n}

Tactic:
← ker_toZModPow,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ (lift f_compat) r - g r ∈ RingHom.ker (toZModPow n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Tactic:
· rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
    use ⟨r, i⟩
    rw [smul_val, Zsqrtd.ext_iff]
    exact ⟨hr, hi⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
have L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡
        xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2] := by
      gcongr
      rw [modEq_zero_iff_dvd, sq]
      gcongr
      apply dvd_mul_of_dvd_right
      rw [← modEq_zero_iff_dvd]
      refine (hy.of_dvd <| dvd_pow_self _ <| by decide).trans ?_
      simp [modEq_zero_iff_dvd]

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b + c - (a + c)).Nonneg

Tactic:
add_sub_add_right_eq_sub

Goal state after:
d : ℕ
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j

Tactic:
delta xz; delta yz
          rw [mul_comm (xn _ _ : ℤ)]
          exact mod_cast (xn_modEq_x2n_add_lem _ n j)

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ m * m

Tactic:
by rw [this]; apply dvd_mul_right

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑p ^ n

Tactic:
rw [discr_prime_pow hζ hirr]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b + c - (a + c)).Nonneg

Tactic:
add_sub_add_right_eq_sub

Goal state after:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case pos
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : 0 ≤ d
⊢ a.re = re 0 ∧ a.im = im 0

pp: case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
· obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
    have : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
    exact divides_sq_eq_zero_z ha

Goal state after:
case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = re 0 ∧ a.im = im 0
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ Irreducible (cyclotomic (p ^ (0 + 1)) ?m.146)

Tactic:
simpa [hirr]

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Tactic:
have hden : ((j / k : ℚ).den : ℤ) ≤ k := by
    convert! le_of_dvd hk₀ (Rat.den_dvd j k)
    exact Rat.intCast_div_eq_divInt _ _

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ xn a1 j % xn a1 n < xn a1 i % xn a1 n

Tactic:
jn,

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ xn a1 n % xn a1 n < xn a1 i % xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
by
        let t := xn_modEq_x4n_sub a1 j42n
        rwa [tsub_tsub_cancel_of_le j4n] at t

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

Goal state before:
pp: case left
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ q.den ≤ ξ.den

Tactic:
rcases eq_or_ne ξ q with (rfl | H)

Goal state after:
case left.inl
ξ : ℚ
hq₀ : 0 < ↑ξ.den
h : |ξ * ↑ξ.den - ↑ξ.num| < 1 / ↑ξ.den
⊢ ξ.den ≤ ξ.den

case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
H : ξ ≠ q
⊢ q.den ≤ ξ.den
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
h : m = 0
⊢ p < p

Tactic:
calc
    p ≤ s.sup id := Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p
    _ < 1 + s.sup id := lt_one_add _
    _ ≤ p := hp₁

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ∈ factoredNumbers s

Tactic:
by
  rw [mem_factoredNumbers]
  exact ⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩

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

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.2

Tactic:
term_convolution f g s n

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2 = ∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂'_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
rw [jacobiTheta₂'_term, norm_mul]

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case a
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t)

Tactic:
rw [show -π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t)
         = π * t * n * (|a| + a) * 2 by ring]

Goal state after:
case a
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ 0 ≤ π * t * ↑n * (|a| + a) * 2
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
by
  have h_re1 : -1 < re (s - 1) := by simpa using P.hk.trans hs
  have h_re2 : -1 < re (s - P.k - 1) := by simpa using hs
  calc
  _ = ∫ (x : ℝ) in Ioi 0, (x : ℂ) ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x
      + ({1} : Set ℝ).indicator (fun _ ↦ P.f₀ - P.f 1) x) :=
    setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ by simp [f_modif_aux1 P hx])
  _ = ∫ (x : ℝ) in Ioi 0, (x : ℂ) ^ (s - 1) • ((Ioo 0 1).indicator
      (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x) := by
    refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))
    rw [indicator_of_notMem hx, add_zero]
  _ = ∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) := by
    simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]
  _ = ∫ x : ℝ in Ioc 0 1, ((x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (x : ℂ) ^ (s - P.k - 1) • P.g₀) := by
    refine setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)
    rw [ofReal_cpow hx.le, ofReal_neg, smul_sub, ← mul_smul, mul_comm, mul_assoc, mul_smul,
      mul_comm, ← cpow_add _ _ (ofReal_ne_zero.mpr hx.ne'), ← sub_eq_add_neg, sub_right_comm]
  _ = (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1)) • P.f₀
        - P.ε • (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - P.k - 1)) • P.g₀ := by
    rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
    · apply Integrable.smul_const
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re1
    · refine (Integrable.smul_const ?_ _).smul _
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re2
  _ = _ := by
      simp_rw [← intervalIntegral.integral_of_le zero_le_one]
      match_scalars
      · simp [integral_cpow (.inl h_re1), zero_cpow (show s ≠ 0 by grind [P.hk, zero_re])]
      · simp [integral_cpow (.inl h_re2), zero_cpow (show s - P.k ≠ 0 by grind [P.hk, ofReal_re])]
        grind

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

Goal state before:
pp: z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
        (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) +
          (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) /
      (2 * ↑π * I) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I)) / (2 * ↑π * I)

Tactic:
refine congr_arg (· / (2 * π * I)) ?_

Goal state after:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht

Goal state after:
case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ ∀ (n : ℤ), ↑n + a ≠ 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ hurwitzZeta a (1 - s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (-↑π * I * s / 2) * expZeta a s + cexp (↑π * I * s / 2) * expZeta (-a) s)

Tactic:
rw [hurwitzZeta, hurwitzZetaEven_one_sub a hs hs', hurwitzZetaOdd_one_sub a hs,
    expZeta, expZeta, Complex.cos, Complex.sin, sinZeta_neg, cosZeta_neg]
  rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
    show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]
  -- these `generalize` commands are not strictly needed for the `ring_nf` call to succeed, but
  -- make it run faster:
  generalize (2 * π : ℂ) ^ (-s) = x
  generalize (↑π * s / 2 * I).exp = y
  generalize (-(↑π * s / 2) * I).exp = z
  ring_nf

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

Goal state before:
pp: case refine_3
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -↑π * ↑n ^ 2 * ↑t = ↑π * I * ↑n ^ 2 * (I * ↑t)

Tactic:
simp [← mul_assoc, mul_comm _ I]

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → M
⊢ (fun n ↦ if Nat.Prime n then f n else 1) = {n | Nat.Prime n}.mulIndicator f

Tactic:
by
  ext; simp [Set.mulIndicator_apply]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)

Tactic:
refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n ↦ ↑n + a
c : ℤ → ℂ := fun n ↦ 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t)) = ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * t)) / 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ x * x + y * y = z * z

Tactic:
← mul_left_inj' (mul_ne_zero hk hk)

Goal state after:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
left

Goal state after:
case inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree

Tactic:
rw [← Polynomial.degree_ne_bot] at ha

Goal state after:
case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ a.degree + (derivative b).degree < a.degree + b.degree
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ (a * b * c).natDegree = (divRadical (a * b * c) * radical (a * b * c)).natDegree

Tactic:
by
      rw [mul_comm _ (radical _), radical_mul_divRadical]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ i ∣ a

pp: case ha
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ Irreducible i

pp: case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ a ≠ 0

Tactic:
· exact dvd_of_mem_normalizedFactors hi

Goal state after:
case ha
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ Irreducible i

case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ a ≠ 0
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
left

Goal state after:
case neg
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := ⋯
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
    b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ normalizedFactors a ⊆ normalizedFactors b

Tactic:
← Multiset.toFinset_subset,

Goal state after:
case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors b).toFinset