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

Goal state before:
pp: case ex
L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih2 : ∀ {ψ : L.BoundedFormula α (n✝ + 1)}, ψ.IsPrenex → (φ✝.toPrenexImp ψ).IsPrenex
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ ((∃' φ✝).toPrenexImp ψ).IsPrenex

Tactic:
exact (ih2 hψ.liftAt).all

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddMonoid.FG M
F : Type u_5
G : Type u_6
inst✝³ : FunLike F M N
inst✝² : AddMonoidHomClass F M N
inst✝¹ : FunLike G M N
inst✝ : AddMonoidHomClass G M N
a b : N
f : F
g : G
⊢ IsSemilinearSet {x | a + f x = b + g x}

Tactic:
by
  rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, h, hh⟩
  rw [AddMonoidHom.mrange_eq_top] at hh
  rw [← image_preimage_eq { x | a + f x = b + g x } hh, preimage_ofPred_eq]
  apply IsSemilinearSet.image
  exact Nat.isSemilinearSet_setOfPred_eq a b (AddMonoidHom.comp f h) (AddMonoidHom.comp g h)

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 ι
i : ι
x y : G i
h : (fun a ↦ ⟦Structure.Sigma.mk f i a⟧) x = (fun a ↦ ⟦Structure.Sigma.mk f i a⟧) y
⊢ x = y

Tactic:
Quotient.eq

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 ι
i : ι
x y : G i
h : (setoid G f) (Structure.Sigma.mk f i x) (Structure.Sigma.mk f i y)
⊢ x = y
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 ι
i j : ι
hij : i ≤ j
x : G i
⊢ ⟦Structure.Sigma.mk f j ((f i j hij) x)⟧ = ⟦Structure.Sigma.mk f i x⟧

Tactic:
Quotient.eq

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 ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)
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 ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
xy : x ≈ y
⊢ (g x.fst) x.snd = (g y.fst) y.snd

Tactic:
by
      obtain ⟨i, hx, hy⟩ := directed_of (· ≤ ·) x.1 y.1
      rw [← Hg x.1 i hx, ← Hg y.1 i hy]
      exact congr_arg _ ((equiv_iff ..).1 xy)

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 : ι → ℕ
⊢ ∑ x_1,
      (⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
        (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1) ≤
    toRatVec x

Tactic:
conv =>
    enter [1, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg, ← Int.cast_smul_eq_zsmul ℚ]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ ∑ x_1, ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1 ≤ toRatVec x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ ∑ x_1, ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1 ≤
    ∑ i, (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i

Tactic:
refine Finset.sum_le_sum fun i _ => ?_

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
x✝ : i ∈ Finset.univ
⊢ ↑⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ • toRatVec ↑i ≤
    (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N : Bundled L.Structure
⊢ ⟦N⟧ ∈ Quotient.mk' '' L.age M → ⟦N⟧ ∈ range fun s ↦ ⟦{ α := ↥((closure L).toFun ↑s), str := inferInstance }⟧

Tactic:
simp only [mem_range, Quotient.eq]
    rintro ⟨P, ⟨⟨s, hs⟩, ⟨PM⟩⟩, hP2⟩
    refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩
    rw [← Embedding.coe_toHom, Finset.coe_image, closure_image PM.toHom, hs, ← Hom.range_eq_map]
    exact ⟨PM.equivRange.symm⟩

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
left✝ : Structure.FG L ↑{ α := ↥S, str := inferInstance }
emb_S : ↥S ↪[L] N
v : M ≃ₚ[L] N := { dom := S, cod := emb_S.toHom.range, toEquiv := emb_S.equivRange }
⊢ Nonempty (M ≃[L] N)

Tactic:
exact ⟨Exists.choose (equiv_between_cg cg_of_countable cg_of_countable
    ⟨v, ((Substructure.fg_iff_structure_fg _).2 S_fg)⟩ (hM.isExtensionPair hN)
      (hN.isExtensionPair hM))⟩

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

Tactic:
mul_one

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, 1 + ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * ↑(p.choose x_1) = 1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 1) * 1 = 2 ^ (n - 1)

Tactic:
mul_one

Goal state after:
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 1) = 2 ^ (n - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 2
⊢ λ (2 ^ n) = 2 ^ (n - 2)

Tactic:
by
  by_cases hn' : n ≤ 2
  · grind [carmichael_two_pow_of_le_two]
  refine carmichael_eq_exponent' _ |>.trans <| dvd_antisymm ?_ ?_
  · have hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1) := by
      rw [card_eq_fintype_card, ZMod.card_units_eq_totient, totient_prime_pow prime_two <| by lia,
        Nat.add_one_sub_one, mul_one]
    have ⟨k, hk, h⟩ := dvd_prime_pow prime_two |>.mp <| hcard ▸ Group.exponent_dvd_nat_card
    have := IsCyclic.iff_exponent_eq_card.not.mp <| ZMod.isCyclic_units_two_pow_iff n |>.not.mpr hn'
    exact h ▸ Nat.pow_dvd_pow 2 (by grind)
  · let five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 <| gcd_pow_right_of_gcd_eq_one rfl
    rw [← ZMod.orderOf_five (n - 2), show n - 2 + 2 = n by lia,
      show (5 : ZMod (2 ^ n)) = five by rfl, orderOf_units]
    exact order_dvd_exponent five

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

Goal state before:
pp: case h.e_a.e_a.e_a.a
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
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (u * x) ^ i * ↑(p.choose i) = ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
calc
      (u * x) ^ i * p.choose i =
        (u * x) ^ (2 + (i - 2)) * p.choose i := by rw [Nat.add_sub_of_le hi']
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p.choose i := by ring_nf
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (p * (p.choose i / p) : ℕ) := by
        rw [Nat.mul_div_cancel' (hp.dvd_choose_self hi.2.2.1 <| by lia)]
      _ = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * p * (p.choose i / p : ℕ) := by
        simp only [Nat.cast_mul]; ring_nf
      _ = p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * (p.choose i / p : ℕ)))) := by
        rw [ha]; ring

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

Goal state before:
pp: ⊢ Λ * 1 = Λ

Tactic:
mul_one

Goal state after:
⊢ Λ = Λ
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f * (↑((⇑n - ⇑(single i 1)) i) + 1) = (coeff n) g * (↑((⇑n - ⇑(single i 1)) i) + 1)
⊢ (coeff n) f = (coeff n) g

Tactic:
Pi.sub_apply,

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f * (↑(n i - (single i 1) i) + 1) = (coeff n) g * (↑(n i - (single i 1) i) + 1)
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inl
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Subsingleton E
⊢ (μ.withDensityᵥ f).variation = μ.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
simp [show f = 0 from Subsingleton.elim _ _]

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

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

Tactic:
mul_one

Goal state after:
case neg.inr.inl.refl
p : ℕ
h0 : ¬2 * p ^ 0 = 0
h1 : ¬2 * p ^ 0 = 1
h4 : ¬2 * p ^ 0 = 4
hn✝ : Even (2 * p ^ 0)
hn : Odd (p ^ 0)
h2 : 0 < 1
⊢ 2 = 2
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ * 1 = ‖f x‖ₑ

Tactic:
mul_one

Goal state after:
case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ = ‖f x‖ₑ
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ _root_.bernoulli n * 1 = _root_.bernoulli n

Tactic:
mul_one

Goal state after:
n : ℕ
⊢ _root_.bernoulli n = _root_.bernoulli n
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ {p ∈ Ico (m + 1) (m + n + 1) | Nat.Prime p}
⊢ p ∣ (m + n).choose m

Tactic:
mem_filter,

Goal state after:
m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ Ico (m + 1) (m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
have H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f n * c n = 0 := by grind

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

Goal state before:
pp: case e'_3
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
⊢ 0 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli (1, n).1 =
    1 - ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1

Tactic:
· simp [field, h₃]
    norm_num

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
have no_prime : 4 ^ n < n * n.centralBinom :=
    Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_large)

Goal state after:
n : ℕ
n_large : 512 ≤ n
no_prime : 4 ^ n < n * n.centralBinom
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case e_a
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'
⊢ ↑p ^ N / ↑p ^ e = ↑p ^ (N - e)

Tactic:
div_eq_iff (pow_ne_zero e hp_ne),

Goal state after:
case e_a
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'
⊢ ↑p ^ N = ↑p ^ (N - e) * ↑p ^ e
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

pp: case neg
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:
case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ (d + 1).factorization p ≤ d - 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = 0 ↔ x < 2

Tactic:
refine ⟨fun h₀ ↦ ?_, theta_eq_zero_of_lt_two⟩
  by_contra! contra
  replace contra : 2 ∈ Ioc 0 ⌊x⌋₊ := by rw [mem_Ioc, le_floor_iff (by grind)]; grind
  have h₁ : log (↑(2 : ℕ) : ℝ) ≤ θ x :=
    single_le_sum (fun p hp ↦ log_nonneg (by aesop)) (by aesop (add simp prime_two))
  have := Real.log_pos one_lt_two
  grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.factorization.support
this : Prime p
⊢ p ∈ n.primesLE

Tactic:
Finsupp.mem_support_iff,

Goal state after:
case refine_1
n p : ℕ
h : n.lcmUpto.factorization p ≠ 0
this : Prime p
⊢ p ∈ n.primesLE
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) - 2 * √x * log x ≤ θ x

Tactic:
by
  grw [psi_ge' (by linarith)]
  linarith [psi_sub_theta_le hx]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖(ψ - θ) x‖ ≤ c * ‖√x‖

Tactic:
Pi.sub_apply,

Goal state after:
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖ψ x - θ x‖ ≤ c * ‖√x‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ 2 ^ 2 ≤ x

Tactic:
norm_num [hx]

Goal state after:
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 ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
conv_lhs at H₂ => rw [Nat.pow_add', Nat.cast_mul]

Goal state after:
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 ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))

Tactic:
exact Units.ext_iff.1 <| SetCoe.ext_iff.2 <|
    zpow_eq_zpow_emod _ pow_card_eq_one' (G := rootsOfUnity n L)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
this : 0 ≤ log x
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x

Tactic:
norm_of_nonneg (show 0 ≤ x / log x by bound),

Goal state after:
ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * (x / log x)
this : 0 ≤ log x
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = (toZModPow m) x

Tactic:
rw [← zmod_cast_comp_toZModPow _ _ h]
  simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ Algebra.discr ℤ ⇑b = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)

Tactic:
rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ))
      ((↑ringOfIntegersEquiv).toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default) *
        (↑ringOfIntegersEquiv).toIntLinearEquiv.symm ((Basis.singleton (Fin 1) ℤ) default)) =
    (Algebra.trace ℤ (𝓞 ℚ)) 1

Tactic:
← AddEquiv.toIntLinearEquiv_symm,

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ))
      ((↑ringOfIntegersEquiv).symm.toIntLinearEquiv ((Basis.singleton (Fin 1) ℤ) default) *
        (↑ringOfIntegersEquiv).symm.toIntLinearEquiv ((Basis.singleton (Fin 1) ℤ) default)) =
    (Algebra.trace ℤ (𝓞 ℚ)) 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) (1 * 1) = (Algebra.trace ℤ (𝓞 ℚ)) 1

Tactic:
mul_one

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) 1 = (Algebra.trace ℤ (𝓞 ℚ)) 1
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
t : (ZMod n)ˣ
this : NeZero ↑n
⊢ minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K ⋯).gen

Tactic:
simp only [IsPrimitiveRoot.powerBasis_gen]

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
t : (ZMod n)ˣ
this : NeZero ↑n
⊢ minpoly K (zeta n K L) = minpoly K (zeta n K L ^ (↑t).val)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inl
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * 1 * (2 ^ k.succ * 1 - 1) / 2) = (-1) ^ (2 ^ k.succ * 1 / 2)

Tactic:
mul_one

Goal state after:
case e_a.inl
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * (2 ^ k.succ - 1) / 2) = (-1) ^ (2 ^ k.succ / 2)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a

Tactic:
mul_one

Goal state after:
a : ℕ
a1 : 1 < a
this : a ≤ a * a
⊢ a ≤ a * a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 n * 1
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Tactic:
mul_one

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 n
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n