mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case refine_1
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ 0 < ε * 2 ^ (-↑m)

pp: case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ ε * 2 ^ (-↑m) ≤ 1

Tactic:
· simpa using ⟨εpos, (ENNReal.zpow_pos (by simp) (by simp) (-↑m))⟩

Goal state after:
case refine_2
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
inst✝³ : PseudoMetricSpace 𝓧
inst✝² : OpensMeasurableSpace 𝓧
inst✝¹ : SecondCountableTopology 𝓧
S : Set (ProbabilityMeasure 𝓧)
inst✝ : CompleteSpace 𝓧
hcomp : IsCompact (closure[ProbabilityMeasure.instTopologicalSpace] S)
hnonempty : Nonempty 𝓧
D : ℕ → 𝓧
hD : DenseRange D
u : ℕ → ℝ
hu_anti : StrictAnti u
hu_pos : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
hcov : ∀ (m : ℕ), ⋃ i, ball (D i) (u m) = univ
ε : ℝ≥0∞
εpos : 0 < ε
hεbound : ε ≤ 1
m : ℕ
⊢ ε * 2 ^ (-↑m) ≤ 1
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic

Goal state before:
pp: X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
m : Measure X
hs : MeasurableSet s
h : ∀ (E : Set X), MeasurableSet E → E ⊆ s → ‖μ E‖ₑ ≤ m E
i : Finpartition ⟨s, ⋯⟩
⊢ m (i.parts.sup Subtype.val) ≤ m s

Tactic:
rw [sup_set_eq_biUnion]
      exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
⊢ False

Tactic:
have A (s : Set X) (hs : MeasurableSet s) (h's : μ.semivariation s = ∞) :
      ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ :=
    exists_one_le_enorm_apply_of_semivariation_eq_top hs h's

Goal state after:
X : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
mX : MeasurableSpace X
μ : VectorMeasure X E
h : μ.semivariation univ = ∞
A :
  ∀ (s : Set X),
    MeasurableSet s → μ.semivariation s = ∞ → ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ
⊢ False
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
⊢ (μ.restrict s).transpose B = (μ.transpose B).restrict s

Tactic:
ext t ht : 1

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
s : Set X
hs : MeasurableSet s
t : Set X
ht : MeasurableSet t
⊢ ((μ.restrict s).transpose B) t = ((μ.transpose B).restrict s) t
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case hbc.h
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∫⁻ (a : X), ENNReal.ofReal ‖f a‖ ∂μ.variation ≤ ∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation

Tactic:
· apply lintegral_mono_ae
      filter_upwards [h] with x hx using ENNReal.ofReal_mono hx

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex
L : Language
α : Type u'
n : ℕ
ψ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih2 : ∀ {φ : L.BoundedFormula α (n✝ + 1)}, φ.IsQF → (φ.toPrenexImpRight φ✝).IsPrenex
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
⊢ (φ.toPrenexImpRight (∃' φ✝)).IsPrenex

Tactic:
exact (ih2 hφ.liftAt).ex

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]

Goal state after:
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✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ unify f (fun a ↦ Structure.Sigma.mk f i (x a)) i ⋯ a = x a

Tactic:
rw [unify]

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✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ (f (Structure.Sigma.mk f i (x a)).fst i ⋯) (Structure.Sigma.mk f i (x a)).snd = x a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ ∃ P s₁' s₂', P.FG ∧ IsSemilinearSet s₁' ∧ s₁ = Subtype.val '' s₁' ∧ IsSemilinearSet s₂' ∧ s₂ = Subtype.val '' s₂'

Tactic:
by
  rcases hs₁.exists_fg_eq_subtypeVal with ⟨P₁, s₁', hP₁, hs₁', rfl⟩
  rcases hs₂.exists_fg_eq_subtypeVal with ⟨P₂, s₂', hP₂, hs₂', rfl⟩
  refine ⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.image _, ?_⟩
    <;> simp_rw [image_image, AddSubmonoid.coe_inclusion]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
w✝ : f.dom ≤ g.dom
eq_fun : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
n : N
hn : n ∈ f.cod
m : ↥f.dom := f.toEquiv.symm ⟨n, hn⟩
this : (f.cod.subtype.comp f.toEquiv.toEmbedding) m = n
⊢ n ∈ g.cod

Tactic:
rw [← this, ← eq_fun]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
w✝ : f.dom ≤ g.dom
eq_fun : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝)) = f.cod.subtype.comp f.toEquiv.toEmbedding
n : N
hn : n ∈ f.cod
m : ↥f.dom := f.toEquiv.symm ⟨n, hn⟩
this : (f.cod.subtype.comp f.toEquiv.toEmbedding) m = n
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion w✝))) m ∈ g.cod
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

Tactic:
intro h_eq
    rcases f with ⟨dom_f, cod_f, equiv_f⟩
    cases h_eq
    exact ⟨rfl, fun _ _ ↦ rfl⟩

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U

Tactic:
have : ∀ (n) (K : PositiveCompacts X),
        ∃ K' : PositiveCompacts X, closure ↑K' ⊆ f n ∩ interior K := by
      refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_
      rw [inter_comm]
      exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
this : ∀ (n : ℕ) (K : PositiveCompacts X), ∃ K', closure ↑K' ⊆ f n ∩ interior ↑K
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ T.IsSatisfiable

Tactic:
by
  rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
  rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm,
    ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOfPred_subset_eq_empty_iff]
  simp

Goal state after:
Module: Mathlib.Topology.Order.IsLocallyClosed

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Ico a b)

Tactic:
by
  rw [← Set.Iio_inter_Ici]
  exact isLocallyClosed_Iio.inter isLocallyClosed_Ici

Goal state after:
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: n : ℕ
⊢ IsAlmostPrime 1 n ↔ Prime n

Tactic:
by
  constructor
  · exact fun h ↦ ArithmeticFunction.cardFactors_eq_one_iff_prime.mp h.2
  · exact fun h ↦ ⟨h.ne_zero, ArithmeticFunction.cardFactors_eq_one_iff_prime.mpr h⟩

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * ↑p * (↑p * u * v) ∣ ↑p ^ p * u ^ p

Tactic:
apply mul_dvd_mul _ hpuv

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * ↑p ∣ ↑p ^ p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(p ^ (n + m + 1)) ∣ ↑(p ^ (n + m)) * a

Tactic:
pow_succ,

Goal state after:
case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(p ^ (n + m) * p) ∣ ↑(p ^ (n + m)) * a
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ i ∈ range (p.succ + 1), eval (↑n) ((monomial i) (_root_.bernoulli (p.succ - i) * ↑(p.succ.choose i))) -
      _root_.bernoulli p.succ

Tactic:
eval_monomial

Goal state after:
n p : ℕ
⊢ ∑ i ∈ range (p + 1), _root_.bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) =
    ∑ x ∈ range (p.succ + 1), _root_.bernoulli (p.succ - x) * ↑(p.succ.choose x) * ↑n ^ x - _root_.bernoulli p.succ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n x : ℕ
hx : x ∈ range n
⊢ ↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x = 0

Tactic:
rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ bernoulli' n = (-1) ^ n * bernoulli n

Tactic:
by
  simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inl
m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
⊢ (m + m + 1)# < 4 ^ (m + m + 1)

Tactic:
rcases m.eq_zero_or_pos with rfl | hm
    · decide
    calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
· rcases Decidable.eq_or_ne n 1 with rfl | hn
    · decide
    · calc
        (n + 1)# = n# := primorial_succ hn ho
        _ < 4 ^ n := ihn n n.lt_succ_self (by grind)
        _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (-x) (bernoulli n) = (-1) ^ n * (eval x (bernoulli n) + ↑n * x ^ (n - 1))

Tactic:
simpa [mul_add] using congr_arg (Polynomial.eval x) (bernoulli_comp_neg_X n)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ bernoulliPowerSeries A * (exp A - 1) = X

Tactic:
by
  ext n
  -- constant coefficient is a special case
  cases n with | zero => simp | succ n =>
  simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
    coeff_one, coeff_exp, map_sub, factorial, if_pos, cast_succ, cast_mul,
    sub_zero, add_eq_zero, if_false, one_ne_zero, and_false, ← map_mul, ← map_sum]
  cases n with | zero => simp | succ n =>
  rw [if_neg n.succ_succ_ne_one]
  have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
  have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
  simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]
  rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
  refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
  rw [mem_antidiagonal] at h
  rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
  simp [field, mul_comm _ (bernoulli x.1), mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x = ∑ n ∈ Icc 0 ⌊x⌋₊, Λ n

Tactic:
rw [psi, ← add_sum_Ioc_eq_sum_Icc]

Goal state after:
x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = Λ 0 + ∑ x ∈ Ioc 0 ⌊x⌋₊, Λ x

x : ℝ
⊢ 0 ≤ ⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : ψ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
⊢ False

Tactic:
have : Λ 2 ≤ ψ x := single_le_sum (fun n _ ↦ vonMangoldt_nonneg (n := n)) contra

Goal state after:
x : ℝ
h₀ : ψ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
this : Λ 2 ≤ ψ x
⊢ False
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
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 <
    ↑(Fintype.card ι).factorial *
      (↑(Fintype.card ι) *
          (Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^
        Fintype.card ι

Tactic:
apply mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _))

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 ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 <
    (↑(Fintype.card ι) *
        (Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^
      Fintype.card ι
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'
⊢ ↑y' < y

Tactic:
rw [y'_def,
      ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)
          _ (him.image _)]

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 ℤ
ι : 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'
⊢ (Finset.image (fun x ↦ ↑x) (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ)).max' ⋯ < y
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₂ : ℕ
⊢ k₂ ≠ 0 → k₂ ≤ N → p₂ ≠ 0 → ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂

Tactic:
hk₂

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
⊢ k₂ ≤ N → p₂ ≠ 0 → ↑p₂ ≤ x → Nat.Prime p₂ → ↑p₂ ≤ x ^ (↑k₂)⁻¹ → p₁ ^ k₁ = p₂ ^ k₂ → k₁ = k₂ ∧ p₁ = p₂
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero.inl
k : ℕ
hk : k > 0
hi : 0 + 1 < 2 * k
inst✝ : Fact (Nat.Prime 2)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / ↑2)
⊢ (Rat.padicValuation 2) (-(2 ^ (2 * k - 2 + 1) / 2)) ≤ 1

Tactic:
pow_succ,

Goal state after:
case succ.zero.inl
k : ℕ
hk : k > 0
hi : 0 + 1 < 2 * k
inst✝ : Fact (Nat.Prime 2)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / ↑2)
⊢ (Rat.padicValuation 2) (-(2 ^ (2 * k - 2) * 2 / 2)) ≤ 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n = ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
trans ∑ ⟨k, p⟩ ∈ Icc 1 N ×ˢ (Ioc 0 ⌊x⌋₊).filter Nat.Prime
    with p ≤ ⌊x ^ (k : ℝ)⁻¹⌋₊, f (p ^ k)
  · refine (sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm
    · simp +contextual [hx, rpow_nonneg, le_floor_iff, ← pos_iff_ne_zero, Prime.isPrimePow,
        one_le_iff_ne_zero, le_rpow_inv_iff_of_pos, isPrimePow_pow_iff, prime_iff]
    · simp +contextual only [hx, rpow_nonneg, le_floor_iff, mem_filter, mem_product, mem_Icc,
        one_le_iff_ne_zero, pos_iff_ne_zero, mem_Ioc, and_imp, Prod.forall, Prod.mk.injEq]
      intro k₁ p₁ hk₁ _ _ _ hp₁ _ k₂ p₂ hk₂ _ _ _ hp₂ _ H
      exact (hp₁.pow_inj' hp₂ hk₁ hk₂ H).symm
    · simp +contextual only [mem_filter, mem_Ioc, hx, le_floor_iff, and_assoc, rpow_nonneg,
        mem_product, mem_Icc, succ_le_iff, exists_prop, Prod.exists, exists_and_left, and_imp]
      rintro b _ hbx ⟨p, k, hp, hk₀, rfl⟩
      rw [cast_pow] at hbx
      refine ⟨k, hk₀, (le_floor ?_).trans hN, p, hp.nat_prime.pos, ?_, hp.nat_prime, ?_, rfl⟩
      · rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow]
        gcongr
        apply (LE.le.trans ?_ hbx)
        exact pow_le_pow_left₀ (by norm_num) (mod_cast hp.nat_prime.two_le) _
      · exact (le_self_pow₀ (mod_cast hp.nat_prime.one_le) hk₀.ne').trans hbx
      · simp_all [le_rpow_inv_iff_of_pos]
    · simp
  · rw [sum_filter, sum_product]
    refine sum_congr rfl fun k _ ↦ ?_
    simp only [sum_ite, not_le, sum_const_zero, add_zero]
    congr 1
    ext p
    simp only [mem_filter, mem_Ioc]
    refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩
    simp_all only [mem_Icc, one_div, true_and, and_true]
    grw [h.1.2, floor_le_floor]
    apply rpow_le_self_of_one_le _ (by bound)
    have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2
    contrapose! this
    apply rpow_lt_one hx this (by bound)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) = ∑ n ∈ Icc 0 ⌊x⌋₊, (log ↑n)⁻¹ * a n

pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log ↑n)⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
· refine sum_congr rfl fun n hn ↦ ?_
    split_ifs with h
    · 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]
    · simp [a, h]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log ↑n)⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 0 - ↑0 ∈ Ideal.span {↑v}

Tactic:
simp only [sub_zero, cast_zero, Submodule.zero_mem]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ a 0 = 0

Tactic:
simp [a, not_prime_zero]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
rw [add_tsub_cancel_of_le h] at t

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)