mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ setToFun (variation μ.toSignedMeasure) ⇑(transpose μ.toSignedMeasure (lsmul ℝ ℝ).flip) ⋯ f = ∫ (x : X), f x ∂μ

Tactic:
MeasureTheory.integral_eq_setToFun

Goal state after:
case inr
X : Type u_2
G : Type u_6
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X → G
h'G : Nontrivial G
⊢ setToFun (variation μ.toSignedMeasure) ⇑(transpose μ.toSignedMeasure (lsmul ℝ ℝ).flip) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ f
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) → ∃ n s, (closure L).toFun (range s) = N

Tactic:
rintro ⟨S, Sfin, hS⟩

Goal state after:
case mp
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Sfin : S.Finite
hS : (closure L).toFun S = N
⊢ ∃ n s, (closure L).toFun (range s) = N
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ (closure L).toFun (⇑f ⁻¹' ↑t) = s

Tactic:
refine map_injective_of_injective hf ?_

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' ↑t)) = Substructure.map f.toHom s
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case neg
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
ψ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
h : ¬φ.Realize v xs
inhabited_h : Inhabited M
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
exact ⟨default, fun h'' => (h h'').elim⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ (closure L).toFun (⇑f ⁻¹' t) = s

Tactic:
refine map_injective_of_injective hf ?_

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' t)) = Substructure.map f.toHom s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
⊢ IsSemilinearSet s

Tactic:
suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    have := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOfPred_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_ofPred_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]

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✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose ⋯ ≤ k
⊢ (f (Classical.choose ⋯) k jk) (funMap F (unify f (fun i_1 ↦ Structure.Sigma.mk f i (x i_1)) (Classical.choose ⋯) ⋯)) =
    (f i k ik) (funMap F x)

Tactic:
simp only [Embedding.map_fun, comp_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✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
F : L.Functions n
i : ι
x : Fin n → G i
k : ι
ik : i ≤ k
jk : Classical.choose ⋯ ≤ k
⊢ funMap F (unify f (fun i_1 ↦ Structure.Sigma.mk f i (x i_1)) k ⋯) = funMap F (⇑(f i k ik) ∘ x)
Module: Mathlib.ModelTheory.Graph

Goal state before:
pp: V : Type u
S : Language.graph.Structure V
inst✝ : V ⊨ Theory.simpleGraph
⊢ (simpleGraphOfStructure V).structure = S

Tactic:
ext
  case funMap n f xs =>
    exact isEmptyElim f
  case RelMap n r xs =>
    match n, r with
    | 2, .adj =>
      rw [iff_eq_eq]
      change RelMap adj ![xs 0, xs 1] = _
      refine congr rfl (funext ?_)
      simp [Fin.forall_fin_two]

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

Goal state before:
pp: case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + ((-hs.floor x i).toNat • ↑i + ∑ j ∈ Finset.univ.erase i, (-hs.floor x j).toNat • ↑j) =
    hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j

Tactic:
Finset.add_sum_erase _ (fun j => (-hs.floor x j).toNat • j.1) (Finset.mem_univ i),

Goal state after:
case mp.refine_4
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : hs.floor x i < 0
⊢ x + ∑ x_1, (-hs.floor x x_1).toNat • ↑x_1 = hs.base + ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • ↑j
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
⊢ L.IsUltrahomogeneous M → L.IsExtensionPair M M

pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsExtensionPair M M → L.IsUltrahomogeneous M

Tactic:
· intro M_homog ⟨f, f_FG⟩ m
    let S := f.dom ⊔ closure L {m}
    have dom_le_S : f.dom ≤ S := le_sup_left
    let ⟨f', eq_f'⟩ := M_homog.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG)
      ((subtype _).comp f.toEquiv.toEmbedding) (inclusion dom_le_S) (h := ⟨subtype _⟩)
    refine ⟨⟨⟨S, f'.toHom.range, f'.equivRange⟩, f_FG.sup (fg_closure_singleton _)⟩,
      subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨dom_le_S, ?_⟩⟩
    ext
    simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, coe_subtype, eq_f',
      Embedding.equivRange_apply, Substructure.coe_inclusion]

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
⊢ L.IsExtensionPair M M → L.IsUltrahomogeneous M
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case h
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
⊢ f = g.toEmbedding.comp S.subtype

Tactic:
rw [← eq]

Goal state after:
case h
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] M
g : M ≃[L] M
dom_le_dom :
  (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ g.toEmbedding.toPartialEquiv.dom
eq :
  g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    f
⊢ g.toEmbedding.toPartialEquiv.cod.subtype.comp
      (g.toEmbedding.toPartialEquiv.toEquiv.toEmbedding.comp (Substructure.inclusion dom_le_dom)) =
    g.toEmbedding.comp S.subtype
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
⊢ (∀ (a a_1 : M),
      Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 0) <
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc default a) a_1)) ((var ∘ Sum.inr) 1) →
        ∃ a_3,
          Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 0) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) ∧
            Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 2) <
              Term.realize (Sum.elim default (Fin.snoc (Fin.snoc (Fin.snoc default a) a_1) a_3)) ((var ∘ Sum.inr) 1)) ↔
    DenselyOrdered M

Tactic:
refine ⟨fun h => ⟨fun a b ab => h a b ab⟩, ?_⟩

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

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

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

Tactic:
· exact admissible_D' r

Goal state after:
case «1».«1»
r : ℕ+
hqr : 3 ≤ r
H : 1 < sumInv {2, 3, r}
⊢ Admissible {2, 3, r}
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.134 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.134 ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ Real.log ↑a + Real.log ↑b = Real.log (↑a * ↑b)

Tactic:
Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')

Goal state after:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ Real.log ↑a + Real.log ↑b = Real.log ↑a + Real.log ↑b
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∀ x ∈ n.divisors, ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n

Tactic:
simp only [and_imp, Ne, mem_divisors]

Goal state after:
n : ℕ
⊢ ∀ (x : ℕ), x ∣ n → ¬n = 0 → ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ orderOf (1 + ↑p) = p ^ n

Tactic:
convert! orderOf_one_add_mul_prime hp hp2 1 _ n
  · simp
  · intro H
    apply hp.ne_one
    simpa using Int.eq_one_of_dvd_one (Int.natCast_nonneg p) H

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
⊢ (coeff n) (pderivFun i (f * g)) = (coeff n) (f • pderivFun i g + g • pderivFun i f)

Tactic:
have h₂ : n + single i 1 < n + single i 1 + single i 1 :=
    lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
⊢ (coeff n) (pderivFun i (f * g)) = (coeff n) (f • pderivFun i g + g • pderivFun i f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
⊢ (pderiv R i) (X j) = Pi.single i 1 j

Tactic:
by
  by_cases h : i = j
  · subst h; simp only [pderiv_X_self, Pi.single_eq_same]
  · grind [pderiv_X_of_ne]

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

Goal state before:
pp: case neg.inl
p m : ℕ
h0 : ¬p ^ m = 0
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
h1 : m < 1
⊢ p ^ m = 1

Tactic:
cases Nat.lt_one_iff.mp h1

Goal state after:
case neg.inl.refl
p : ℕ
h0 : ¬p ^ 0 = 0
h2 : ¬p ^ 0 = 2
h4 : ¬p ^ 0 = 4
hn : Odd (p ^ 0)
h1 : 0 < 1
⊢ p ^ 0 = 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: ⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      _root_.bernoulli 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64

Tactic:
bernoulli_eq_bernoulli'_of_ne_one (by decide : 3 ≠ 1),

Goal state after:
⊢ 1 * ↑(Nat.choose 3 0) * (1 / 4) ^ (3 - 0) + -1 / 2 * ↑(Nat.choose 3 1) * (1 / 4) ^ (3 - 1) +
        1 / 6 * ↑(Nat.choose 3 2) * (1 / 4) ^ (3 - 2) +
      bernoulli' 3 * ↑(Nat.choose 3 3) * (1 / 4) ^ (3 - 3) =
    3 / 64
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (monomial x✝¹) ((↑((n + 1 - x✝¹).choose x✝) * _root_.bernoulli x✝) • ↑((n + 1).choose x✝¹))

Tactic:
← smul_monomial

Goal state after:
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
| (↑((n + 1 - x✝¹).choose x✝) * _root_.bernoulli x✝) • (monomial x✝¹) ↑((n + 1).choose x✝¹)
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
← sum_flip _,

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

Goal state before:
pp: ⊢ bernoulli' 4 = -1 / 30

Tactic:
have : Nat.choose 4 2 = 6 := by decide -- shrug
  rw [bernoulli'_def]
  norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.refine_2
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) = ↑n / 2

Tactic:
simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]

Goal state after:
case succ.succ.refine_2
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ↑n + 1 + 1 - (↑0 + 1) - (↑n + 1 + 1) * (1 / 2) = ↑n / 2
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)

Tactic:
Nat.div_le_self

Goal state after:
case h
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ Finset.range (2 * n + 1) ⊆ Finset.range (2 * n + 1)
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
not_le,

Goal state after:
case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n / 3 < x
⊢ x ^ n.centralBinom.factorization x = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : p = 2 ∧ d = 2
⊢ (d + 1).factorization p ≤ d - 1

Tactic:
obtain ⟨rfl, rfl⟩ := hcase
    simp [Nat.factorization_eq_zero_of_not_dvd (by decide : ¬(2 ∣ 3))]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 < ↑n

pp: case refine_2
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}

Tactic:
· simp only [mem_filter] at hn; exact_mod_cast hn.2.one_lt

Goal state after:
case refine_2
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : b.natDegree ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
rwa [mod_eq, sub_self, map_zero, Int.cast_zero]

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
⊢ 2 < p

Tactic:
exact (Prime.odd_iff Fact.out).mp <| Prime.odd_of_ne_two Fact.out hp2

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
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
⊢ 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:
hAlg

Goal state after:
case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
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
⊢ ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den

Tactic:
induction k using Nat.strong_induction_on with

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑p ∣ x
⊢ x.zmodRepr = 0

Tactic:
apply zmodRepr_unique _ _ (Nat.Prime.pos Fact.out)

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hx : ↑p ∣ x
⊢ x - ↑0 ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ i) * ↑(p ^ k) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑(p ^ i) ≠ 0

Tactic:
simp [NeZero.ne p]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).re = (↑(2 * a) * pellZd a1 (n + 1)).re

Tactic:
simp [dz_val, az]

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n)) * ↑a + (↑a * ↑a - 1) * (↑(xn a1 n) + ↑(yn a1 n) * ↑a) + ↑(xn a1 n) =
    2 * ↑a * (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).im = (↑(2 * a) * pellZd a1 (n + 1)).im

Tactic:
simp [dz_val, az]

Goal state after:
case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n) + (↑(xn a1 n) + ↑(yn a1 n) * ↑a) * ↑a + ↑(yn a1 n) =
    2 * ↑a * (↑(xn a1 n) + ↑(yn a1 n) * ↑a)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
y n : ℕ
this : 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n)
⊢ 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣
    ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n) +
        ↑(2 * a) * (yz a1 (n + 1) * (↑a - ↑y) + ↑(y ^ (n + 1)) - xz a1 (n + 1)) -
      (yz a1 n * (↑a - ↑y) + ↑(y ^ n) - xz a1 n)

Tactic:
exact _root_.dvd_sub (dvd_add this <| (x_sub_y_dvd_pow _ (n + 1)).mul_left _)
      (x_sub_y_dvd_pow _ n)

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

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

Tactic:
have : m * m = d * (n * n) := by
        refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_
        simpa [mul_comm, mul_left_comm, mul_assoc] using h

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