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

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ z ∈ f (x + y)

Tactic:
rw [hf _ hy]

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ x + y + z ∈ s
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:
closure_union,

Goal state after:
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₁ ⊔ (closure L).toFun t₂ = N₁ ⊔ N₂
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (S ∪ {h.some}) = N

Tactic:
closure_union,

Goal state after:
case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun S ⊔ (closure L).toFun {h.some} = N
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:
closure_union,

Goal state after:
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₁ ⊔ (closure L).toFun t₂ = N₁ ⊔ N₂
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable ((l : ℕ) × L.Functions l)
s : L.Substructure M
⊢ s.CG ↔ Countable ↥s

Tactic:
refine ⟨?_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
  rintro ⟨s, h, rfl⟩
  exact h.substructure_closure L

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
h : FG L M
f : M →[L] N
hs : Function.Surjective ⇑f
⊢ FG L N

Tactic:
by
  rw [← Hom.range_eq_top] at hs
  rw [fg_def, ← hs]
  exact h.range f

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
⊢ IsSemilinearSet {x | a + f x = b + g x}

Tactic:
apply isSemilinearSet_of_isSlice

Goal state after:
M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
⊢ IsSlice {x | a + f x = b + g x}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
by
  rcases hs with ⟨a, t, ht, rfl⟩
  refine ⟨_, _, (fg_iff _).2 ⟨insert a t, rfl, ht.insert a⟩,
    ⟨⟨_, mem_closure_of_mem (mem_insert a t)⟩, _, ht.preimage Subtype.val_injective.injOn, rfl⟩, ?_⟩
  rw [← coe_subtype, image_vadd_distrib, subtype_apply, ← coe_map, AddMonoidHom.map_mclosure]
  congr
  ext x
  simpa using mem_closure_of_mem ∘ mem_insert_of_mem a

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
le_fg : f ≤ g
le_gf : g ≤ f
⊢ f = g

Tactic:
let ⟨dom_f, cod_f, equiv_f⟩ := f
  cases _root_.le_antisymm (dom_le_dom le_fg) (dom_le_dom le_gf)
  cases _root_.le_antisymm (cod_le_cod le_fg) (cod_le_cod le_gf)
  convert! rfl
  exact Equiv.injective_toEmbedding ((subtype _).comp_injective (subtype_toEquiv_inclusion le_fg))

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
⊢ Function.Injective fun f ↦ f.toPartialEquiv

Tactic:
intro _ _ h
  ext
  rw [PartialEquiv.ext_iff] at h
  rcases h with ⟨_, H⟩
  exact H _ (Substructure.mem_top _)

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
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding

Tactic:
#adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
    these two `simp` calls cannot be combined. -/

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
rw [← toRatVec_inj, hs.toRatVec_fract_eq, hs.toRatVec_fract_eq]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
f : ↑hs.basisSet → ℕ
⊢ toRatVec hs.base +
      ∑ i, Int.fract ((hs.basis.repr (toRatVec (x + ∑ i, f i • ↑i) - toRatVec hs.base)) i) • toRatVec ↑i =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (∃ i ∈ hs.fundamentalDomain \ {hs.base}, ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = i + y) →
    hs.fract x ≠ hs.base

Tactic:
· rintro ⟨u, ⟨hu, hu'⟩, y, hy, y', hy', heq⟩
      apply congr_arg hs.fract at heq
      rw [hs.fract_add_of_mem_closure hy', hs.fract_add_of_mem_closure hy,
        hs.fract_eq_self_of_mem_fundamentalDomain hu] at heq
      rwa [heq]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
⊢ ∃ f', f = f'.comp g

Tactic:
let ⟨r⟩ := h
  let s := r.comp g
  let ⟨t, eq⟩ := M_homog s.toHom.range (S_FG.range s.toHom) (f.comp s.equivRange.symm.toEmbedding)
  use t.toEmbedding.comp r
  change _ = t.toEmbedding.comp s
  ext x
  have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩
  simp only [Embedding.comp_apply,
    coe_subtype] at eq'
  simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]
  apply (Embedding.equivRange (Embedding.comp r g)).injective
  ext
  simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
M_CG : Structure.CG L M
h : L.IsExtensionPair M M
⊢ L.IsUltrahomogeneous M

Tactic:
S

Goal state after:
case mpr
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 → ∀ (f : ↥S ↪[L] M), ∃ g, f = g.toEmbedding.comp S.subtype
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: ⊢ Language.order.card = 1

Tactic:
simp [card]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝⁵ : L.IsOrdered
inst✝⁴ : L.Structure M
inst✝³ : LE M
inst✝² : Language.order.Structure M
inst✝¹ : Language.order.OrderedStructure M
inst✝ : L.orderLHom.IsExpansionOn M
x : Fin 2 → M
⊢ RelMap leSymb x ↔ x 0 ≤ x 1

Tactic:
by
    rw [← orderLHom_leSymb L, LHom.IsExpansionOn.map_onRelation, relMap_leSymb]

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_next : ℕ → PositiveCompacts X → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure ↑(K_next n K) ⊆ f n ∩ interior ↑K
⊢ ∃ K, (∀ (n : ℕ), K (n + 1) ≤ K n) ∧ (∀ (n : ℕ), closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U

Tactic:
use Nat.rec K₀ K_next

Goal state after:
case h
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_next : ℕ → PositiveCompacts X → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure ↑(K_next n K) ⊆ f n ∩ interior ↑K
⊢ (∀ (n : ℕ), (fun t ↦ Nat.rec K₀ K_next t) (n + 1) ≤ (fun t ↦ Nat.rec K₀ K_next t) n) ∧
    (∀ (n : ℕ), closure ↑((fun t ↦ Nat.rec K₀ K_next t) (n + 1)) ⊆ f n) ∧ closure ↑((fun t ↦ Nat.rec K₀ K_next t) 0) ⊆ U
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
⊢ Language.empty.age M = {S | Finite ↑S}

Tactic:
ext S
    simp only [age, Structure.fg_iff_finite, mem_ofPred_eq, and_iff_left_iff_imp]
    intro hS
    simp

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hs : [p, q, r].SortedLE
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r

Tactic:
by simpa using hs.pairwise

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

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

Tactic:
rw [add_comm, add_pow]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y, ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * 1 ^ (p - m) * ↑(p.choose m) = 1 + ↑p * u * (x + v * y)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((trunc R n) (pderivFun i f)) =
    MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

Tactic:
coeff_trunc

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
⊢ (if m✝ < n then (coeff m✝) (pderivFun i f) else 0) = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inr.inl
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * (2 * n)))ˣ

Tactic:
← mul_assoc

Goal state after:
case inr.inr.inl
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * 2 * n))ˣ
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ ((trunc n) ((d⁄dX R) f)).coeff d = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

Tactic:
coeff_trunc

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ (if d < n then (coeff d) ((d⁄dX R) f) else 0) = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

pp: case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n

Tactic:
· norm_num [h]

Goal state after:
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
← mul_assoc

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 +
      (f ↑⌊1⌋₊ * c ⌊1⌋₊ +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * ∑ k ∈ Icc 0 ⌊1⌋₊, c k -
          ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
Nat.floor_one,

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 +
      (f ↑1 * c 1 +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * ∑ k ∈ Icc 0 1, c k -
          ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
← mul_assoc

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

Goal state before:
pp: case e'_2
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
⊢ ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli p.1 = ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli' p.1

Tactic:
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h

Goal state after:
case e'_2
n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
h' : p ∈ antidiagonal n.succ
h'' : p ≠ (1, n)
⊢ ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli p.1 = ↑((p.1 + p.2).choose p.2) / (↑p.2 + 1) * bernoulli' p.1
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
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
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x

Tactic:
← div_le_one (rpow_pos_of_pos four_pos x),

Goal state after:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
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
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) / 4 ^ x ≤ 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)!

pp: 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

Tactic:
· exact factorial_mul_factorial_dvd_factorial h.le

Goal state after:
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: p l : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (∑ v ∈ Ico 1 p, ↑v ^ l + if p - 1 ∣ l then 1 else 0) = 0

Tactic:
have hbij : (∑ v ∈ Ico 1 p, (v : ZMod p) ^ l) = ∑ u : (ZMod p)ˣ, (u : ZMod p) ^ l :=
    Finset.sum_bij'
      (fun v hv ↦ Units.mk0 (v : ZMod p) (mt (ZMod.natCast_eq_zero_iff v p).mp (by
        grind [not_dvd_of_pos_of_lt])))
      (fun u _ ↦ (u : ZMod p).val)
      (fun _ _ ↦ Finset.mem_univ _)
      (fun u _ ↦ by grind [u.ne_zero, ZMod.val_ne_zero, ZMod.val_lt])
      (fun v hv ↦ by simp [ZMod.val_cast_of_lt (Finset.mem_Ico.mp hv).2])
      (fun u _ ↦ Units.ext (ZMod.natCast_zmod_val _))
      (fun _ _ ↦ rfl)
  rw [hbij, FiniteField.sum_pow_units, ZMod.card]
  grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
have hrw : (p : ℚ) ^ N / M = (p : ℚ) ^ (N - e) / M' := by
    rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]
    congr 1
    rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
hrw : ↑p ^ N / ↑M = ↑p ^ (N - e) / ↑M'
⊢ pIntegral p (↑p ^ N / ↑M)
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₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

pp: case neg
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 : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
· obtain ⟨i₀, i₁, i_ne, mod_eq⟩ :=
      exists_eq_polynomial le_rfl b le_b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb
    refine ⟨i₀, i₁, i_ne, ?_⟩
    rwa [mod_eq, sub_self, map_zero, Int.cast_zero]

Goal state after:
case neg
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 : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x ≤ ψ x

Tactic:
by
  by_cases! h : x < 2
  · rw [theta_eq_zero_of_lt_two h, psi_eq_zero_of_lt_two h]
  rw [psi_eq_theta_add_sum_theta h]
  simp only [le_add_iff_nonneg_right]
  exact sum_nonneg fun _ _ ↦ theta_nonneg _

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

Goal state before:
pp: case refine_2.refine_1
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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ ↑(abv ((bS.repr (∑ x, (rs k x • bS x - rs j x • bS x))) i)) ≤ ↑(abv (rs k i - rs j i))

Tactic:
apply le_of_eq
    congr
    simp_rw [map_sum, map_sub, map_smul, Finset.sum_apply',
      Finsupp.sub_apply, Finsupp.smul_apply, Finset.sum_sub_distrib, Basis.repr_self_apply,
      smul_eq_mul, mul_boole, Finset.sum_ite_eq', Finset.mem_univ, if_true]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1

Tactic:
rcases eq_or_ne ‖(x.zmodRepr : ℤ_[p])‖ ‖x‖ with H | H

Goal state after:
case inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ = ‖x‖
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1

case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1