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

Goal state before:
pp: case mp
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))

Tactic:
induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
       =>  _ 

Goal state after:
case mp.h
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
n : ℕ
ih' :
  ∀ m < n,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
g : M → ℕ
hn : g i = n
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp
s : Set ℕ
hs : IsProperSemilinearSet s
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
isProperSemilinearSet_iff

Goal state after:
case mp
s : Set ℕ
hs : ∃ S, (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ ↑S
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case pos
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : x < k
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x

pp: case neg
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : ¬x < k
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x

Tactic:
· exact Or.inl ⟨hx, hx'⟩

Goal state after:
case neg
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : {x | x ∈ s ∧ x < k}.Finite
h₂ : {x | x ∈ s ∧ k ≤ x ∧ x < k + p}.Finite
x : ℕ
hx : x ∈ s
hx' : ¬x < k
⊢ x ∈ s ∧ x < k ∨ ∃ x_1, ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ a, x_1 + a * p = x
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.FG
hN₂ : N₂.FG
t₁ : Set M
ht₁ : t₁.Finite ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Finite ∧ (closure L).toFun t₂ = N₂
⊢ (closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N₁ N₂ : L.Substructure M
hN₁ : N₁.CG
hN₂ : N₂.CG
t₁ : Set M
ht₁ : t₁.Countable ∧ (closure L).toFun t₁ = N₁
t₂ : Set M
ht₂ : t₂.Countable ∧ (closure L).toFun t₂ = N₂
⊢ (closure L).toFun (t₁ ∪ t₂) = N₁ ⊔ N₂

Tactic:
rw [closure_union, ht₁.2, ht₂.2]

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
⊢ ∀ {m : ℕ} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ

Tactic:
intro m

Goal state after:
L : Language
α : Type u'
n : ℕ
P : {m : ℕ} → L.BoundedFormula α m → Prop
φ : L.BoundedFormula α n
hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ
hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P (∀' ψ)
hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P (∃' φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, φ₁ ⇔[∅] φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
⊢ ∀ {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
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 ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f ((Quotient.out ∘ x) a).fst i r) ((Quotient.out ∘ x) a).snd)

Tactic:
change _ ≈ Structure.Sigma.mk f i (f (Quotient.out (x a)).fst i r (Quotient.out (x a)).snd)

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 ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : ↑hs.basisSet
⊢ hs.floor (x + ∑ j, f ↑j • ↑j) i = hs.floor x i + ↑(f ↑i)

Tactic:
simp only [floor]
  rw [map_add, ← sub_add_eq_add_sub, ← Finset.sum_coe_sort]
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply]

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

Tactic:
let out := Quotient.out (s := DirectLimit.setoid G f)

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 ∈ ⊤
out : Quotient (setoid G f) → Σˣ f := Quotient.out
⊢ x ∈ S
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
Kn : K.Nonempty
left✝ : ∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
cq : (Quotient.mk' '' K).Countable
hfg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
⊢ ∃ M, Countable ↑M ∧ L.age ↑M = K

Tactic:
obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep

Goal state after:
case mpr
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG L ↑M
Kn : (L.age ↑M).Nonempty
left✝ : ∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)
cq : (Quotient.mk' '' L.age ↑M).Countable
hfg : ∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1
hp : Hereditary (L.age ↑M)
jep : JointEmbedding (L.age ↑M)
⊢ ∃ M_1, Countable ↑M_1 ∧ L.age ↑M_1 = L.age ↑M
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝² : L.IsOrdered
inst✝¹ : L.Structure M
h : M ⊨ L.linearOrderTheory
inst✝ : DecidableRel fun a b ↦ RelMap leSymb ![a, b]
⊢ leSymb.total ∈ L.linearOrderTheory

Tactic:
simp [linearOrderTheory]

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ((Formula.equivSentence.symm φ).Realize fun a ↦ ↑(L.con a)) ↔ φ ∈ p

Tactic:
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)

Goal state after:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType ↑p
φ : L[[α]].Sentence
⊢ ↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯)) ⊨ φ ↔ ↑M ⊨ φ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: 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
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)

Tactic:
use a * x ^ 2 * ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p,
    (u * x) ^ (i - 2) * (p.choose i / p : ℕ) + b * x ^ p

Goal state after:
case h
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
⊢ 1 +
      ((u * x) ^ 1 * ↑(p.choose 1) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
          (u * x) ^ p * ↑(p.choose p))) =
    1 +
      ↑p * u *
        (x +
          v *
            (a * x ^ 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
              b * x ^ p))
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Tactic:
intro m

Goal state after:
n m : ℕ
⊢ m ∣ n → ¬n = 0 → ↑(μ m) * -Real.log ↑(n / m) = ↑(μ m) * Real.log ↑m - ↑(μ m) * Real.log ↑n
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ C r • pderivFun i f + 0 = C r * pderivFun i f

Tactic:
add_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ C r • pderivFun i f = C r * pderivFun i f
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! ≠ 0

Tactic:
rintro h

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ False
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ bernoulli n =
    ∑ j ∈ range (n + 1), (monomial (n + 0 - j)) (_root_.bernoulli (n - (n + 0 - j)) * ↑(n.choose (n + 0 - j)))

Tactic:
add_zero,

Goal state after:
n : ℕ
⊢ bernoulli n = ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Tendsto π' atTop atTop

Tactic:
apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
  simp [Set.range_eq_univ.mpr surjective_primeCounting']

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesBelow

Tactic:
intros n m _ p

Goal state after:
n m : ℕ
a✝ : n ≤ m
p : ℕ
⊢ p ∈ n.primesBelow → p ∈ m.primesBelow
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesLE

Tactic:
intros n m _ p

Goal state after:
n m : ℕ
a✝ : n ≤ m
p : ℕ
⊢ p ∈ n.primesLE → p ∈ m.primesLE
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑((n + 1).choose n) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)

Tactic:
choose_succ_self_right

Goal state after:
n : ℕ
this :
  ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
⊢ ↑(n + 1) * ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x +
      ↑(n + 1) * (1 - ∑ x ∈ range n, Rat.divInt (↑(n.choose x)) (Int.subNatNat n x + 1) * bernoulli' x) =
    ↑(n + 1)
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf.hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) log

Tactic:
exact strictConcaveOn_log_Ioi.concaveOn.subset
          (Set.Ioi_subset_Ioi (by norm_num)) (convex_Ioi 0.5)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := ⋯
⊢ ∀ x ∈ range q.succ,
    bernoulli x / ↑x ! * (coeff (q - x + 1)) (exp ℚ ^ n) =
      bernoulli x * ↑((q + 1).choose x) * ↑n ^ (q + 1 - x) / ↑(q + 1)!

Tactic:
intro m

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
⊢ m ∈ range q.succ →
    bernoulli m / ↑m ! * (coeff (q - m + 1)) (exp ℚ ^ n) =
      bernoulli m * ↑((q + 1).choose m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! * (↑n ^ (q - m + 1) * (↑(q - m + 1)!)⁻¹)

Tactic:
rw [mul_comm ((n : ℚ) ^ (q - m + 1)), ← mul_assoc _ _ ((n : ℚ) ^ (q - m + 1)), ← one_div,
      mul_one_div, div_div, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul]

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * (↑(q + 1)! / (↑m ! * ↑(q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / (↑m ! * ↑(q + 1 - m)!) * ↑n ^ (q + 1 - m)

case hnm
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ m ! * (q + 1 - m)! ∣ (q + 1)!

case hn
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ ↑(m ! * (q + 1 - m)!) ≠ 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case refine_1
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n ↦ (algebraMap ℚ ℚ) (bernoulli n / ↑n !)) = PowerSeries.mk fun p ↦ bernoulli p / ↑p !) ∨
    (PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)) = 0

Tactic:
left
      congr

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

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ ↑j
⊢ (A i₁).coeff j = (A i₀).coeff j

pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
· rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj),
      coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
⊢ pIntegral p (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))

Tactic:
have 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) := by rw [hpow]; field_simp [hp_ne]; ring

Goal state after:
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)
⊢ pIntegral p (bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1))
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 : ℚ := ↑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 (↑p * (↑((2 * k).choose (2 * m)) * P / (2 * ↑k - 2 * ↑m + 1)))

Tactic:
exact pIntegral_mul (Int.padicValuation_le_one p p) hcmp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
· rw [Valuation.map_neg]
      refine pIntegral_pow_div two_ne_zero <|
         (factorization_eq_zero_of_lt ?_).trans_le (by lia)
      exact (Prime.odd_iff Fact.out).mp <| Prime.odd_of_ne_two Fact.out hp2

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
by
  by_cases! hx : x < 2
  · rw [psi_eq_zero_of_lt_two hx, theta_eq_zero_of_lt_two hx, sub_zero, abs_zero]
    bound
  rw [psi_eq_theta_add_sum_theta hx, add_sub_cancel_left]
  apply le_trans <| abs_sum_le_sum_abs ..
  simp_rw [abs_of_nonneg <| theta_nonneg _]
  trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt
  · gcongr with i hi
    apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))
    rw [sqrt_eq_rpow]
    gcongr; simp_all
  simp only [sum_const, card_Icc, reduceSubDiff, nsmul_eq_mul]
  calc
  _ ≤ (log x / log 2) * (log 4 * √x) := by
    gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound
  _ = (log 4 / log 2) * x.sqrt * x.log := by field
  _ = _ := by
    congr
    rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
    field

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case mpr
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
⊢ FunctionField F K

Tactic:
let b := Module.finBasis Ft K
    refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite
    intro c x; convert! (this (e.symm c) x).symm; simp only [e.apply_symm_apply]

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

Goal state after:
case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A (⇑b ∘ ⇑f.symm) = discr A ⇑b

Tactic:
by
  rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ↑p ≤ √x
⊢ log √x ≤ log ↑p + log √x

Tactic:
simp [log_natCast_nonneg]

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

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
⊢ ∃ k, k ≠ 0 ∧ ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ k, k ≠ 0 ∧ ↑p ^ (-↑k) < ε