mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case of_isQF
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
f : F
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α n✝
hQF : φ✝.IsQF
xs : Fin n✝ → M
⊢ φ✝.Realize v xs → φ✝.Realize (⇑f ∘ v) (⇑f ∘ xs)

Tactic:
| of_isQF hQF =>

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case insert
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
S : Set (Set M)
a✝¹ : Set M
s✝ : Set (Set M)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsSemilinearSet s) → IsSemilinearSet (⋂₀ s✝)
hS' : IsSemilinearSet a✝¹ ∧ ∀ a ∈ s✝, IsSemilinearSet a
⊢ IsSemilinearSet (⋂₀ insert a✝¹ s✝)

Tactic:
simpa using hS'.1.inter (ih hS'.2)

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
⊢ ∀ (x : M) (h : x ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom),
    (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
        ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x, h⟩) =
      { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
        ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x, ⋯⟩)

Tactic:
intro _ _

Goal state after:
case refl.a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
cod✝ : L.Substructure N
toEquiv✝ : ↥{ carrier := Set.univ, fun_mem := ⋯ } ≃[L] ↥cod✝
x✝ : M
h✝ : x✝ ∈ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.dom
⊢ (PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.cod.subtype
      ((PartialEquiv.toEmbeddingOfEqTop ⋯).toPartialEquiv.toEquiv ⟨x✝, h✝⟩) =
    { dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.cod.subtype
      ({ dom := { carrier := Set.univ, fun_mem := ⋯ }, cod := cod✝, toEquiv := toEquiv✝ }.toEquiv ⟨x✝, ⋯⟩)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ ∀ (b : L.Substructure (DirectLimit G f)),
    (∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ b) → ⊤ ≤ b

Tactic:
intro S hS x _

Goal state after:
case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
S : L.Substructure (DirectLimit G f)
hS : ∀ (i : ι), Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯)) ≤ S
x : DirectLimit G f
a✝ : x ∈ ⊤
⊢ x ∈ S
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 α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ⇑(Equiv.prodComm β α).symm '' ↑↑f ⊆ ↑↑f'

Tactic:
← Finset.coe_image,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑(Finset.image ⇑(Equiv.prodComm β α).symm ↑f) ⊆ ↑↑f'
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `S)
   []
   []
   ":="
   («term_⊔_»
    `f.dom
    "⊔"
    (Term.app
     `closure
     [`L
      (choice
       («term{_}» "{" [`m] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields [(Term.structInstField (Term.structInstLVal `m []) [])])
        (Term.optEllipsis [])
        []
        "}"))])))))

Goal state after:
case mp
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
M_homog : L.IsUltrahomogeneous M
f : M ≃ₚ[L] M
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a b : M
⊢ Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 0) <
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 1) →
    ∃ a_2,
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_2)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_2)) ((var ∘ Sum.inr) 2) ∧
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_2)) ((var ∘ Sum.inr) 2) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_2)) ((var ∘ Sum.inr) 1)

Tactic:
ab

Goal state after:
L : Language
M : Type w'
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
h : DenselyOrdered M
a b : M
ab :
  Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 0) <
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) b)) ((var ∘ Sum.inr) 1)
⊢ ∃ a_1,
    Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 0) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) ∧
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 2) <
        Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) b) a_1)) ((var ∘ Sum.inr) 1)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
(Tactic.tacticLet__
 "let"
 (Term.letConfig [])
 (Term.letDecl
  (Term.letIdDecl
   (Term.letId `S)
   []
   []
   ":="
   («term_⊔_»
    `f.dom
    "⊔"
    (Term.app
     `closure
     [`L
      (choice
       («term{_}» "{" [`m] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields [(Term.structInstField (Term.structInstLVal `m []) [])])
        (Term.optEllipsis [])
        []
        "}"))])))))

Goal state after:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
f : M ≃ₚ[L] N
f_FG : f.dom.FG
m : M
S : L.Substructure M := f.dom ⊔ (closure L).toFun {m}
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: k l m n : ℕ
hm : k.IsAlmostPrime m
hn : l.IsAlmostPrime n
⊢ (k + l).IsAlmostPrime (m * n)

Tactic:
refine ⟨mul_ne_zero hm.1 hn.1, ?_⟩
  rw [ArithmeticFunction.cardFactors_mul hm.1 hn.1, hm.2, hn.2]

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case «1»
q r : ℕ+
hqr : q ≤ r
H : 1 < sumInv {2, q, r}
hq4 : q ∈ Finset.Ico 2 4
⊢ Admissible {2, q, r}

Tactic:
conv at hq4 => change q ∈ ({2, 3} : Multiset ℕ+)

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

Goal state before:
pp: case refine_2
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)
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ (n + 1)

Tactic:
apply orderOf_eq_prime_pow

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)
⊢ ¬(1 + ↑p ^ m * ↑a) ^ p ^ n = 1

case hfin
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)
⊢ (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:

Tactic:
∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ
    _ = ∑ j ∈ Q, ‖∫ᵛ x in j, f x ∂[B; μ]‖ₑ := by
      simp only [Q]
      rw [Finset.sum_image_of_pairwise_eq_zero]; swap
      · rintro ⟨i, p⟩ hi ⟨j, q⟩ hj hijpq h'ij
        simp only [Finset.coe_sigma, SimpleFunc.coe_range, mem_sigma_iff, mem_range,
          SetLike.mem_coe] at hi hj
        suffices H : Disjoint p q by
          have : Disjoint (p ∩ s) (q ∩ s) := H.mono inter_subset_left inter_subset_left
          rw [← h'ij, disjoint_self] at this
          simp [this]
        rcases eq_or_ne i j with rfl | hij
        · simp only [ne_eq, Sigma.mk.injEq, heq_eq_eq, true_and] at hijpq
          exact Pdisj i hi.2 hj.2 hijpq
        · have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind
          exact this.mono (Pg i p hi.2) (Pg j q hj.2)
      apply Finset.sum_congr rfl
      rintro ⟨i, p⟩ hi
      simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hi
      rw [restrict_restrict _ (Pmeas i p hi.2) hs]
    _ = ∑ j ∈ Q, ‖μ.withDensity f B j‖ₑ :=
      Finset.sum_congr rfl (fun t ht ↦ by rw [withDensity_apply hf])
    _ ≤ (μ.withDensity f B).variation s := by
      apply le_variation _ hs
      · intro t ht
        simp only [Finset.mem_image, Finset.mem_sigma, SimpleFunc.mem_range, mem_range,
          Sigma.exists, ↓existsAndEq, true_and, exists_and_right, Q] at ht
        rcases ht with ⟨p, -, rfl⟩
        exact inter_subset_right
      · intro t ht u hu htu
        simp only [Finset.coe_image, Finset.coe_sigma, SimpleFunc.coe_range, mem_image,
          mem_sigma_iff, mem_range, SetLike.mem_coe, Sigma.exists, ↓existsAndEq, true_and,
          exists_and_right, Q] at ht hu
        rcases ht with ⟨p, ⟨i, hi⟩, rfl⟩
        rcases hu with ⟨q, ⟨j, hj⟩, rfl⟩
        have hpq : p ≠ q := by grind only
        suffices H : Disjoint p q from H.mono inter_subset_left inter_subset_left
        rcases eq_or_ne (g i) (g j) with hij | hij
        · rw [← hij] at hj
          exact Pdisj (g i) hi hj hpq
        · have : Disjoint (g ⁻¹' {g i}) (g ⁻¹' {g j}) := by grind
          exact this.mono (Pg (g i) p hi) (Pg (g j) q hj)

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case hfC
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
⊢ ∀ᵐ (x : X) ∂μ.withDensity fun x ↦ ‖f x‖ₑ, ‖‖f x‖⁻¹ • f x‖ ≤ 1

Tactic:
· filter_upwards with x using by simp [norm_smul, inv_mul_le_one]

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

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1

Tactic:
rintro ⟨p, m, -, odd, -, eq⟩

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
odd : Odd p
eq : 2 * n = p ^ m
⊢ False
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inr.ha
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬IsCyclic (ZMod (4 * n))ˣ

Tactic:
isCyclic_units_four_mul_iff

Goal state after:
case neg.inr.inr.ha
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬(n = 0 ∨ n = 1)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
simp only [add_tsub_cancel_of_le, mem_range_succ_iff.mp hx, cast_sub]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 1
hgt : 1 < n
⊢ bernoulli n = bernoulli' n

Tactic:
cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

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) * n !) * (1 / ↑n !))

Tactic:
rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]

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) =
    (aeval t) ((monomial n) (↑n + 1))
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) =
    (aeval t) ((monomial n) (↑n + 1))

Tactic:
rw [← sum_bernoulli, Finset.mul_sum, map_sum]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
⊢ Tendsto (fun n ↦ ∑ k ∈ Icc 0 n, f ↑k * c k) atTop (𝓝 (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
have h : (fun n : ℕ ↦ ∫ (x : ℝ) in (1 : ℝ)..n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop]
      (fun n : ℕ ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) := by
    filter_upwards [eventually_ge_atTop 1] with _ h
    rw [← integral_of_le (Nat.one_le_cast.mpr h)]
  have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (1 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
      atTop (𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
    refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
    exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int
  refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
  rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]
  exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ √(2 * ↑n)

Tactic:
exact_mod_cast Real.nat_sqrt_le_real_sqrt

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf
x y : ℝ
hxy : x ≤ y
⊢ ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log ↑i

Tactic:
exact fun p _ _ ↦ log_natCast_nonneg p

Goal state after:
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)

Goal state after:
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 =
    ∑ x ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)

R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match x with
      | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊,
      match x with
      | (k, p) => f (p ^ k)) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ∃ T,
    bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
      ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
have hcast : (↑((∑ v ∈ Ico 1 p, (v : ℤ) ^ (2 * k)) +
      (if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 :=
    mod_cast sum_pow_add_indicator_eq_zero (p := p) _
  obtain ⟨T, hT_int⟩ := (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).mp hcast
  use T
  have hT : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) + vonStaudtIndicator (2 * k) p =
      p * T := by unfold vonStaudtIndicator; exact_mod_cast hT_int
  have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
  have hAlg : bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / p =
      T - (∑ i ∈ range (2 * k), bernoulli i * ((2 * k + 1).choose i) *
        (p : ℚ) ^ (2 * k + 1 - i) / (2 * k + 1)) / p := by
    field_simp [hp_ne]; linarith [hT, sum_pow_filter_eq_faulhaber p hk]
  rw [hAlg]; congr 1; simpa using faulhaber_sum_div_prime_eq

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Tactic:
have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑↑(r.den.gcd p) % ↑p = ↑(↑r.den * r.den.gcdA p + ↑p * r.den.gcdB p) % ↑p
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Monotone x.appr

Tactic:
by
  apply monotone_nat_of_le_succ
  intro n
  dsimp [appr]
  split_ifs; · rfl
  apply Nat.le_add_right

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) < ε
⊢ (toZModPow n) ((lift f_compat) r) - (toZModPow n) (g r) = 0

Tactic:
← RingHom.comp_apply,

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) < ε
⊢ ((toZModPow n).comp (lift f_compat)) r - (toZModPow n) (g r) = 0
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) < ε
⊢ ((toZModPow n).comp (lift f_compat)) r - (toZModPow n) (g r) = 0

Tactic:
← RingHom.comp_apply,

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) < ε
⊢ ((toZModPow n).comp (lift f_compat)) r - ((toZModPow n).comp g) r = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d

Tactic:
by
  simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy

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

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0

Tactic:
norm_def,

Goal state after:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re - d * z.im * z.im = 0
⊢ z = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b c : ℤ√↑d
hab : a ≤ b
hbc : b ≤ c
⊢ a ≤ c

Tactic:
by simpa [sub_add_sub_cancel'] using! hab.add hbc

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

Goal state before:
pp: case pos
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)
heven : Even (φ (p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n

pp: case neg
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)
heven : ¬Even (φ (p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n

Tactic:
· exact ⟨1, p ^ (k - 1) * ((p - 1) * k - 1), by rw [heven.neg_one_pow]; simp⟩

Goal state after:
case neg
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)
heven : ¬Even (φ (p ^ k) / 2)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n