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

Goal state before:
pp: 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
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (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))
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))

Tactic:
by_cases! hfg : ∀ j ∈ t', f j ≤ g j

Goal state after:
case pos
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 → ℕ
ih' :
  ∀ m < g i,
    ∀ (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))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))

case neg
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 → ℕ
ih' :
  ∀ m < g i,
    ∀ (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))
hfg : ∃ j ∈ t', g j < f j
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case h₁
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
⊢ ↑(NNReal.mk ‖B‖ ⋯) ≤ ‖B‖ₑ

Tactic:
simp [← coe_nnnorm]

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

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
hμ : ¬μ.variation = 0
this : (ae μ.variation).NeBot
⊢ 0 ≤ C

Tactic:
obtain ⟨x, hx⟩ := h.exists

Goal state after:
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
hμ : ¬μ.variation = 0
this : (ae μ.variation).NeBot
x : X
hx : ‖f x‖ ≤ C
⊢ 0 ≤ C
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S : { S // S.FG }
⊢ ∀ ⦃a₂ : { S // S.FG }⦄, g S = g a₂ → S = a₂

Tactic:
S'

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Countable M
g : { S // S.FG } → Finset M := fun S ↦ Exists.choose ⋯
S S' : { S // S.FG }
⊢ g S = g S' → S = S'
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝² : Preorder ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
α : Type u_1
i : ι
x : α → G i
a : α
⊢ (f (Structure.Sigma.mk f i (x a)).fst i ⋯) (Structure.Sigma.mk f i (x a)).snd = x a

Tactic:
apply DirectedSystem.map_self

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
hy : y ∈ closure hs.basisSet
⊢ (hs.basis.repr (toRatVec x - toRatVec hs.base)) i ≤
    (hs.basis.repr (toRatVec x - toRatVec hs.base)) i + (hs.basis.repr (toRatVec y)) i

Tactic:
le_add_iff_nonneg_right

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
hy : y ∈ closure hs.basisSet
⊢ 0 ≤ (hs.basis.repr (toRatVec y)) i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mem
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y✝ : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
y : ι → ℕ
hy : y ∈ t
⊢ (hs.basis.repr (hs.basis ⟨y, ⋯⟩)) i = 0

Tactic:
simpa [Finsupp.single_apply, ← Subtype.val_inj] using ne_of_mem_of_not_mem hy hi

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 : M ≃ₚ[L] N
h : f.dom = ⊤
⊢ (PartialEquiv.toEmbeddingOfEqTop h).toPartialEquiv = f

Tactic:
rcases f with ⟨_, _, _⟩
  cases h
  apply PartialEquiv.ext
  · intro _ _
    rfl
  · rfl

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ (lift L ι (fun i ↦ ↥(S i)) (fun x x_1 h ↦ Substructure.inclusion ⋯) (fun x ↦ (S x).subtype) ⋯).toHom.range = ⨆ i, S i

Tactic:
range_lift,

Goal state after:
L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ ⨆ i, (S i).subtype.toHom.range = ⨆ i, S i
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
b : β
hb : ∀ x ∈ Slt, x < b
hb' : ∀ y ∈ Sgt, b < y
x : α
hx : x ∈ insert a S
y : α
hy : y ∈ insert a S
hxy : ⟨x, hx⟩ < ⟨y, hy⟩
hxS : x ∈ S
hyS : y ∈ S
⊢ (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨x, hx⟩ < (fun x ↦ if hx : ↑x ∈ S then f ⟨↑x, hx⟩ else b) ⟨y, hy⟩

Tactic:
simpa only [hxS, hyS, ↓reduceDIte, OrderEmbedding.lt_iff_lt, Subtype.mk_lt_mk]

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

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + ↑i + y + z' = hs.base + z
⊢ hs.floor x i < 0

Tactic:
mem_closure_singleton

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : ∃ n, n • ↑i = y
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + ↑i + y + z' = hs.base + z
⊢ hs.floor x i < 0
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : L.IsOrdered
inst✝² : L.Structure M
inst✝¹ : Preorder M
inst✝ : L.OrderedStructure M
t₁ t₂ : L.Term (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ (t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂

Tactic:
by
  simp [Term.lt, lt_iff_le_not_ge]

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

Goal state before:
pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i

Tactic:
mem_closure_singleton

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : ∃ n, n • ↑i = y
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ↑F ≤ nhds { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ }

Tactic:
nhds_generateFrom

Goal state after:
case refine_3
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ↑F ≤
    ⨅ s ∈ {s | { toTheory := {φ | T.typesWith φ ∈ F}, subset' := ⋯, isMaximal' := ⋯ } ∈ s ∧ s ∈ range T.typesWith},
      Filter.principal s
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv (D' n)

Tactic:
D',

Goal state after:
case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < sumInv {2, 2, n}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hpuv : ↑p * u * v ∣ u ^ p
x a : R
ha : u = v * a
⊢ ∃ 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:
obtain ⟨b, hb⟩ := hpuv

Goal state after:
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)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b

Tactic:
rw [← Nat.cast_add_one, ← Nat.le_floor_iff' (Nat.succ_ne_zero k)]
    exact (Set.mem_Ico.mp hk).2

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ n.divisors, Λ i = Real.log ↑n

Tactic:
by
  refine recOnPrimeCoprime ?_ ?_ ?_ n
  · simp
  · intro p k hp
    rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
      vonMangoldt_apply_one]
    simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
  intro a b ha' hb' hab ha hb
  simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
  rw [mul_divisors_filter_prime_pow hab, filter_union,
    sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb, Nat.cast_mul,
    Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]

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

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
obtain rfl | hn0 := eq_or_ne n 0

Goal state after:
case inl
⊢ IsCyclic (ZMod (4 * 0))ˣ ↔ 0 = 0 ∨ 0 = 1

case inr
n : ℕ
hn0 : n ≠ 0
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
rw [h4]

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod 4)ˣ ↔ 4 = 0 ∨ 4 = 1 ∨ 4 = 2 ∨ 4 = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (4 = p ^ m ∨ 4 = 2 * p ^ m)
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
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m

Tactic:
Nat.mul_left_cancel_iff zero_lt_two,

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 : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
convert! this using 1

Goal state after:
case e'_2
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!))

case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: k : ℕ
⊢ derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k

Tactic:
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]

Goal state after:
k : ℕ
⊢ ∑ x ∈ range (k + 1 + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ i ∈ range (k + 1), (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
⊢ ∏ x ∈ Ico 0 (m + n + 1) with Nat.Prime x, x =
    (∏ x ∈ Ico 0 (m + 1) with Nat.Prime x, x) * ∏ x ∈ Ico (m + 1) (m + n + 1) with Nat.Prime x, x

Tactic:
rw [← prod_union, ← filter_union, Ico_union_Ico_eq_Ico]

Goal state after:
case hab
m n : ℕ
⊢ 0 ≤ m + 1

case hbc
m n : ℕ
⊢ m + 1 ≤ m + n + 1

m n : ℕ
⊢ Disjoint ({p ∈ Ico 0 (m + 1) | Nat.Prime p}) ({p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p})
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli n = 0

Tactic:
rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg.inr
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 0)

Tactic:
rw [bernoulli_eq_zero_of_odd] <;> grind

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) =
    (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
rw [mul_left_comm, ← map_mul]

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) =
    t ^ n * (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
refine ⟨i₀, i₁, ne, fun k ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : abv.IsAdmissible
A : Fin (h✝.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h✝.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(abv (A i₁ (e.symm k) % b - A i₀ (e.symm k) % b)) < abv b • ε
k : ι
⊢ ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
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 : ℕ
hj : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hd : d ≤ b.natDegree
this : b.natDegree - d < j.succ
⊢ b.natDegree - j.succ < d

Tactic:
rwa [tsub_lt_iff_tsub_lt hd hbj] at this

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ((Icc 1 n).sup fun a ↦ (id a).factorization p) ≤ log p n

pp: case refine_2
n p : ℕ
hp : Prime p
this : 1 < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

Tactic:
· simp only [Finset.sup_le_iff, mem_Icc, and_imp]
    exact fun m _ h ↦ le_log_of_pow_le this (le_of_dvd (by grind) (ordProj_dvd m p) |>.trans h)

Goal state after:
case refine_2
n p : ℕ
hp : Prime p
this : 1 < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ (↑(filter Nat.Prime (Icc 1 n))).PairwiseDisjoint fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))

Tactic:
pairwiseDisjoint_iff

Goal state after:
n : ℕ
⊢ ∀ ⦃i : ℕ⦄,
    i ∈ ↑(filter Nat.Prime (Icc 1 n)) →
      ∀ ⦃j : ℕ⦄,
        j ∈ ↑(filter Nat.Prime (Icc 1 n)) →
          (image (fun x ↦ i ^ x) (Icc 1 (Nat.log i n)) ∩ image (fun x ↦ j ^ x) (Icc 1 (Nat.log j n))).Nonempty → i = j
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ ↑k ≤ log x / log 2

Tactic:
rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow]

Goal state after:
case refine_3.refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ log (2 ^ k) ≤ log x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
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 < ε
⊢ ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)

Tactic:
have := normBound_pos abv bS

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
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 < ε
this : 0 < normBound abv bS
⊢ ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case e_a.e_a
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log 4 / log 2 = 2

Tactic:
(by norm_num : (4 : ℝ) = 2 ^ 2),

Goal state after:
case e_a.e_a
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log (2 ^ 2) / log 2 = 2
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
f : (↥R[x])[X]
hnezero : f ≠ 0
halg : (aeval y) f = 0
⊢ (Transcendental.algEquivAdjoin hy) (swap ((Transcendental.algEquivAdjoin hx).symm f)) ≠ 0

Tactic:
simpa only [map_ne_zero_iff _ (AlgEquiv.injective _)]

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‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1

Tactic:
constructor <;> intro h <;> rw [← h] at this ⊢

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

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