mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : AddMonoid.FG M
F : Type u_5
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective ⇑g
⊢ IsSemilinearSet (⇑g ⁻¹' ⇑f ⁻¹' s)

Tactic:
← preimage_comp,

Goal state after:
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : AddMonoid.FG M
F : Type u_5
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective ⇑g
⊢ IsSemilinearSet (⇑f ∘ ⇑g ⁻¹' s)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : DirectLimit G f
xy : (g (Quotient.out x).fst) (Quotient.out x).snd = (g (Quotient.out y).fst) (Quotient.out y).snd
⊢ x = y

Tactic:
obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.out.1 y.out.1

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : DirectLimit G f
xy : (g (Quotient.out x).fst) (Quotient.out x).snd = (g (Quotient.out y).fst) (Quotient.out y).snd
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
⊢ x = y
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
let D : Sum X Y → Order.Cofinal (FGEquiv L M N) := fun p ↦
    Sum.recOn p (fun x ↦ ext_dom.definedAtLeft x) (fun y ↦ ext_cod.definedAtRight y)

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
⊢ ⇑(OrderEmbedding.ofStrictMono (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⋯) ∘ Set.inclusion ⋯ = ⇑f

Tactic:
· ext x
    simp only [OrderEmbedding.coe_ofStrictMono,
      Function.comp_apply, Finset.coe_mem, ↓reduceDIte, Subtype.coe_eta]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ (DirectLimit.of L ι G f i) ((f (out x).fst i ⋯) (out x).snd) = x

Tactic:
DirectLimit.of_apply,

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
hx : x ∈ ↑s
⊢ ⟦Structure.Sigma.mk f i ((f (out x).fst i ⋯) (out x).snd)⟧ = x
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝¹ : Finite ↥S
this✝ : Infinite { x // x ∉ S }
this : Finite ↥f.toHom.range
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
have : Infinite { x // x ∉ f.toHom.range } := ((Set.toFinite _).infinite_compl).to_subtype

Goal state after:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
I4 :
  ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ
Q : Finset (Set X) := Finset.image (fun p ↦ p.snd ∩ s) (g.range.sigma P)
i : E
p : Set X
j : E
q : Set X
hijpq : ⟨i, p⟩ ≠ ⟨j, q⟩
h'ij : ⟨i, p⟩.snd ∩ s = ⟨j, q⟩.snd ∩ s
hi : (∃ y, g y = i) ∧ p ∈ P i
hj : (∃ y, g y = j) ∧ q ∈ P j
H : Disjoint p q
⊢ ‖∫ᵛ (x : X) in ⟨i, p⟩.snd ∩ s, f x ∂[B; μ]‖ₑ = 0

Tactic:
by
          have : Disjoint (p ∩ s) (q ∩ s) := H.mono inter_subset_left inter_subset_left
          rw [← h'ij, disjoint_self] at this
          simp [this]

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
⊢ ∃ M, p ∈ T.realizedTypes (↑M) α

Tactic:
by
  obtain ⟨M⟩ := p.isMaximal.1
  refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩
  refine SetLike.ext fun φ => ?_
  simp only [CompleteType.mem_typeOf]
  refine
    (@Formula.realize_equivSentence_symm_con _
      ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
      (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
        (p.isMaximal.mem_iff_models φ).symm)
  rfl

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr

Tactic:
Admissible

Goal state after:
pqr : Multiset ℕ+
⊢ (∃ q r, A' q r = pqr) ∨ (∃ r, D' r = pqr) ∨ E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr → 1 < sumInv pqr
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv {2, 2, n}

Tactic:
sumInv_pqr

Goal state after:
case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < sumInv {2, 3, 3}

Tactic:
sumInv_pqr

Goal state after:
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < sumInv {2, 3, 4}

Tactic:
sumInv_pqr

Goal state after:
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < sumInv {2, 3, 5}

Tactic:
sumInv_pqr

Goal state after:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ sumInv {p, q, r} ≤ 1

Tactic:
sumInv_pqr

Goal state after:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ sumInv {2, q, r} ≤ 1

Tactic:
sumInv_pqr

Goal state after:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 6 ≤ r
⊢ sumInv {2, 3, r} ≤ 1

Tactic:
sumInv_pqr

Goal state after:
r : ℕ+
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}

Tactic:
have hr6 : r < 6 := lt_six H

Goal state after:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
hr6 : r < 6
⊢ Admissible {2, 3, r}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h.e_a.e_a.e_a
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) =
    ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
      ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
congr! 1 with i hi
    simp only [Finset.mem_erase, ne_eq, Finset.mem_range] at hi
    have hi' : 2 ≤ i := by lia
    calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = (n - 1).primesLE

Tactic:
cases n <;> simp [primesLE]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i =
    ∑ x ∈ range (d + 1 + 1), ((d + 2).choose x * x) • X ^ (x - 1)

Tactic:
simp [sum_range_succ']

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range n, ↑(n.choose k) * bernoulli k = if n = 1 then 1 else 0

Tactic:
by
  cases n with | zero => simp | succ n =>
  cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * (algebraMap ℚ A) ↑(n + 1)

Tactic:
mul_comm (t ^ n),

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (algebraMap ℚ A) ↑(n + 1) * t ^ n
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
n : ℕ
h : abv.IsAdmissible
this : DecidableEq R
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
induction n with
  | zero =>
    intro ε _hε b _hb A
    refine ⟨0, 1, ?_, ?_⟩
    · simp
    rintro ⟨i, ⟨⟩⟩
  | succ n ih =>
  intro ε hε b hb A
  let M := h.card ε
  -- By the "nicer" pigeonhole principle, we can find a collection `s`
  -- of more than `M ^ n` remainders where the first components lie close together:
  obtain ⟨s, s_inj, hs⟩ :
    ∃ s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ,
      Function.Injective s ∧ ∀ i₀ i₁, (abv (A (s i₁) 0 % b - A (s i₀) 0 % b) : ℝ) < abv b • ε := by
    -- We can partition the `A`s into `M` subsets where
    -- the first components lie close together:
    obtain ⟨t, ht⟩ :
      ∃ t : Fin (M ^ n.succ).succ → Fin M,
        ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ 0 % b - A i₀ 0 % b) : ℝ) < abv b • ε :=
      h.exists_partition hε hb fun x ↦ A x 0
    -- Since the `M` subsets contain more than `M * M^n` elements total,
    -- there must be a subset that contains more than `M^n` elements.
    obtain ⟨s, hs⟩ :=
      Fintype.exists_lt_card_fiber_of_mul_lt_card (f := t)
        (by simpa only [Fintype.card_fin, pow_succ'] using Nat.lt_succ_self (M ^ n.succ))
    have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]
    refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩
    · simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h
    · have (i : Fin (M ^ n).succ) : t (Finset.toList {x | t x = s})[i.castLE this] = s :=
        (Finset.mem_filter.mp ((Finset.mem_toList (s := {x | t x = s})).mp (List.getElem_mem _))).2
      simp_rw [this]
  -- Since `s` is large enough, there are two elements of `A ∘ s`
  -- where the second components lie close together.
  obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))
  refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
  · exact hs k₀ k₁
  · exact h i

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case hx
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ⋯
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
⊢ pIntegral p (↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))

Tactic:
have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /
        (2 * k - 2 * m + 1) =
        (p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by
      rw [hpow]; ring

Goal state after:
case hx
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ↑p ^ (2 * k - 2 * m - 1)
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
hpow_mul :
  ↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k - 2 * ↑m + 1) =
    ↑p * (↑((2 * k).choose (2 * m)) * P / (2 * ↑k - 2 * ↑m + 1))
⊢ pIntegral p (↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (x ∉ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))) → Λ x = 0

Tactic:
simp only [mem_biUnion, mem_filter, mem_Icc, mem_image, not_exists, not_and, and_imp,
        vonMangoldt_eq_zero_iff, isPrimePow_nat_iff]
      contrapose!
      rintro ⟨p, k, hp, hk, rfl⟩
      simp only [mem_Icc] at hx
      have hpn : p ≤ n := (le_of_dvd (by lia) (dvd_pow_self p hk.ne')).trans hx.2
      exact ⟨p, ⟨hp.one_le, hpn, hp, ⟨k, ⟨by lia, le_log_of_pow_le hp.one_lt hx.2, rfl⟩⟩⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ (↑(filter Nat.Prime (Icc 1 n))).PairwiseDisjoint fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))

Tactic:
rw [pairwiseDisjoint_iff]

Goal state after:
n : ℕ
⊢ ∀ ⦃i : ℕ⦄,
    i ∈ ↑(filter Nat.Prime (Icc 1 n)) →
      ∀ ⦃j : ℕ⦄,
        j ∈ ↑(filter Nat.Prime (Icc 1 n)) →
          (image (fun x ↦ i ^ x) (Icc 1 (Nat.log i n)) ∩ image (fun x ↦ j ^ x) (Icc 1 (Nat.log j n))).Nonempty → i = j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n ≤ ↑(π n) * log ↑n

Tactic:
rw [psi_eq_sum_mul_log_prime, ← primesLE_card_eq_primeCounting, ← nsmul_eq_mul, ← sum_const]
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  gcongr with p hp
  refine le_log_of_pow_le (mod_cast (prime_of_mem_primesLE hp).pos) ?_
  exact_mod_cast pow_log_le_self p hn

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁶ : k₁ ≤ N
a✝⁵ : p₁ ≠ 0
a✝⁴ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝³ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝² : k₂ ≤ N
a✝¹ : p₂ ≠ 0
a✝ : ↑p₂ ≤ x
⊢ Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
hp₂

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝⁶ : k₁ ≤ N
a✝⁵ : p₁ ≠ 0
a✝⁴ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
a✝³ : ↑p₁ ≤ x ^ (↑k₁)⁻¹
k₂ p₂ : ℕ
hk₂ : k₂ ≠ 0
a✝² : k₂ ≤ N
a✝¹ : p₂ ≠ 0
a✝ : ↑p₂ ≤ x
hp₂ : Nat.Prime p₂
⊢ ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ AntitoneOn (b x) (Set.Ici 1)

Tactic:
intro n hn m hm hnm; unfold b
  simp only [Set.mem_Ici] at hn hm
  rcases le_or_gt x 1 with h | h
  · repeat rw [theta_eq_zero_of_le_one (rpow_le_one hx h (by positivity))]
  apply theta_mono (monotone_rpow_of_base_ge_one h.le _)
  field_simp
  norm_num [hnm]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
p : F[X]
hp : ↑((algebraMap F[X] ↥(ringOfIntegers F K)) p) = ↑0
⊢ p = 0

Tactic:
Subalgebra.coe_zero

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
p : F[X]
hp : ↑((algebraMap F[X] ↥(ringOfIntegers F K)) p) = 0
⊢ p = 0
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁵ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁴ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝³ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁵.toSMul
this✝² : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝¹ : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝ : SMul ↥F⟮x⟯ ↥Fxy := this✝².toSMul
this : FiniteDimensional ↥F⟮y⟯ ↥Fyx
⊢ FiniteDimensional (↥Fyx) K

Tactic:
have := FiniteDimensional.adjoin_algebraMap_X (F := F) (K := K)
    unfold Fyx
    rw [adjoin_simple_comm]
    have : IsScalarTower F⟮x⟯ Fxy K := isScalarTower_mid' F⟮x⟯⟮y⟯
    exact .right F⟮x⟯ Fxy K

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (ψ - θ) =O[atTop] Real.sqrt

Tactic:
simp_rw [isBigO_iff, Pi.sub_apply, norm_eq_abs, eventually_atTop]
  obtain ⟨C, hC⟩ := psi_sub_theta_le_mul_sqrt
  refine ⟨C, 0, fun x _ ↦ ?_⟩
  have := theta_le_psi x
  rw [abs_of_nonneg (by positivity), abs_of_nonneg (by positivity)]
  exact hC x

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ 1 = (log ↑n)⁻¹ * a n

Tactic:
have : log n ≠ 0 := log_ne_zero_of_pos_of_ne_one (mod_cast h.pos) (mod_cast h.ne_one)
      simp [a, h, field]

Goal state after: