mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
⊢ cmp a ↑(G b) = cmp (↑(F a)) b

Tactic:
rcases (F a).prop with ⟨f, hf, ha⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
val✝¹ : Encodable α
val✝ : Encodable β
to_cofinal : α ⊕ β → Cofinal (PartialIso α β) := fun p ↦ Sum.recOn p (definedAtLeft β) (definedAtRight α)
our_ideal : Ideal (PartialIso α β) := idealOfCofinals default to_cofinal
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a ↦ funOfIdeal a our_ideal ⋯
G : (b : β) → { a // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun b ↦ invOfIdeal b our_ideal ⋯
a : α
b : β
f : PartialIso α β
hf : f ∈ our_ideal
ha : (a, ↑(F a)) ∈ ↑f
⊢ cmp a ↑(G b) = cmp (↑(F a)) b
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ↑j ∈ hs.basisSet \ {↑i}

Tactic:
simpa using

Goal state after:
case mp.refine_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
j : ↑hs.basisSet
hj : j ∈ Finset.univ.erase i
⊢ ¬j = i
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ IsAlmostPrime 1 p

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Prime p
⊢ Prime p
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p q : ℕ
hp : Prime p
hq : Prime q
⊢ IsAlmostPrime 2 (p * q)

Tactic:
simpa using

Goal state after:
p q : ℕ
hp : Prime p
hq : Prime q
⊢ IsAlmostPrime 2 (p * q)
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ IsAlmostPrime 2 (p ^ 2)

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Prime p
⊢ IsAlmostPrime 2 (p * p)
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:
simpa using

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

Goal state before:
pp: n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ

Tactic:
exact IsCyclic.iff_exponent_eq_card.mp <| ZMod.isCyclic_units_two_pow_iff n |>.mpr hn

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

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

Tactic:
by
  rw [carmichael_two_pow_of_le_two_eq_totient hn]
  interval_cases n <;> decide

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

Goal state before:
pp: n : ℕ
⊢ (Λ * ↑ζ) n = log n

Tactic:
rw [coe_mul_zeta_apply, vonMangoldt_sum]

Goal state after:
n : ℕ
⊢ Real.log ↑n = log n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0

Tactic:
simpa using

Goal state after:
n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : ↑p ∣ 1
⊢ p = 1

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
H : ↑p ∣ 1
⊢ p = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ n ≠ 0

Tactic:
simpa using

Goal state after:
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬n = 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this✝ : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this : NeZero n
⊢ Odd (φ n)

Tactic:
simpa using

Goal state after:
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
this✝ : Nat.Coprime 4 n
h : (Nat.card (ZMod 4)ˣ).Coprime (Nat.card (ZMod n)ˣ)
this : NeZero n
⊢ Odd (φ n)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
n : σ →₀ ℕ
⊢ (coeff n) ((pderiv R i) (X j)) = (coeff n) 0

Tactic:
simpa using

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
n : σ →₀ ℕ
⊢ (if n + single i 1 = single j 1 then ↑(n i) + 1 else 0) = 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_1.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ p ^ n.factorization p ≠ 1

Tactic:
simpa using

Goal state after:
case neg.refine_1.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ ¬p = 1
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ constantCoeff ((⇑(d⁄dX R))^[n] f) = ↑n ! * (coeff n) f

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ constantCoeff ((⇑(d⁄dX R))^[n] f) = ↑n ! * (coeff n) f
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case h₂
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
x : E
y : F
⊢ ‖B.flip y‖₊ ≤ ‖y‖₊

Tactic:
apply ContinuousLinearMap.opNNNorm_le_bound

Goal state after:
case h₂
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖x‖₊ * ‖y‖₊
x : E
y : F
⊢ ∀ (x : E), ‖(B.flip y) x‖₊ ≤ ‖y‖₊ * ‖x‖₊
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inr.ha
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬IsCyclic (ZMod (2 * (2 * n)))ˣ

pp: case neg.inr.inr.hb
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬((∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1)

Tactic:
· rw [← mul_assoc, show 2 * 2 = 4 from rfl, isCyclic_units_four_mul_iff]
    lia

Goal state after:
case neg.inr.inr.hb
n : ℕ
h0 : ¬2 * (2 * n) = 0
h1 : ¬2 * (2 * n) = 1
h2 : ¬2 * (2 * n) = 2
h4 : ¬2 * (2 * n) = 4
hn✝ : Even (2 * (2 * n))
hn : Even (2 * n)
⊢ ¬((∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * (2 * n) = 2 * x ^ x_1)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case 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
s : Set X
hs : MeasurableSet s
x : X
hx : f x ≠ 0
⊢ ‖f x‖ ≠ 0

Tactic:
simpa using

Goal state after:
case 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
s : Set X
hs : MeasurableSet s
x : X
hx : f x ≠ 0
⊢ ¬f x = 0
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: 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‖ₑ ≠ 0

Tactic:
simpa using

Goal state after:
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 = 0
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case succ
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale ↑k) (exp A)
⊢ exp A ^ (k + 1) = (rescale ↑(k + 1)) (exp A)

Tactic:
simpa using

Goal state after:
case succ
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
h : exp A ^ k = (rescale ↑k) (exp A)
⊢ exp A ^ (k + 1) = exp A ^ k * exp A
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
by_cases h : n = 1

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

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ (coeff (n + 1, 0).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff (p.1, p.2 + 1).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff (n + 1)) (exp A * X)

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ ∑ x ∈ antidiagonal n,
      (algebraMap ℚ A) (bernoulli' x.1 / ↑x.1!) * ((algebraMap ℚ A) (↑x.2!)⁻¹ * (algebraMap ℚ A) (↑x.2 + 1)⁻¹) =
    (algebraMap ℚ A) (↑n !)⁻¹
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
this : (bernoulli n).comp (1 + X) = bernoulli n + n • X ^ (n - 1)
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℚ
this : (bernoulli n).comp (1 + X) = bernoulli n + n • X ^ (n - 1)
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inl
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : (coeff n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ -bernoulli' n = bernoulli' n

Tactic:
split_ifs at h

Goal state after:
case pos
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h✝ : n = 1
h : (coeff n) (B - (rescale (-1)) B) = 1
⊢ -bernoulli' n = bernoulli' n

case neg
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h✝ : ¬n = 1
h : (coeff n) (B - (rescale (-1)) B) = 0
⊢ -bernoulli' n = bernoulli' n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0

Tactic:
simpa using

Goal state after:
case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
⊢ B * (exp ℚ - 1) = X * exp ℚ

Tactic:
simpa using

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
⊢ B * (exp ℚ - 1) = X * exp ℚ
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (-x) (bernoulli n) = (-1) ^ n * (eval x (bernoulli n) + ↑n * x ^ (n - 1))

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℚ
⊢ eval (-x) (bernoulli n) = (-1) ^ n * eval x (bernoulli n) + (-1) ^ n * (↑n * x ^ (n - 1))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ (bernoulli n).comp (1 - X) = (-1) ^ n * bernoulli n

Tactic:
by
  cases n with
  | zero => simp
  | succ n =>
    trans ((bernoulli (n + 1)).comp (1 + X)).comp (-X)
    · simp [comp_assoc, sub_eq_add_neg]
    simp [bernoulli_comp_one_add_X, bernoulli_comp_neg_X, neg_pow (X : Polynomial ℚ)]
    ring

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (1 - x) (bernoulli n) = (-1) ^ n * eval x (bernoulli n)

Tactic:
simpa using

Goal state after:
n : ℕ
x : ℚ
⊢ eval (1 - x) (bernoulli n) = (-1) ^ n * eval x (bernoulli n)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
simpa using

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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : ¬K.Nonempty
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume

Tactic:
rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
    exact integrableOn_empty

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 0, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
x✝ : ℕ
⊢ ?m.254 x✝ = ∫ (t : ℝ) in Set.Ioc 0 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [← integral_of_le (Nat.cast_nonneg _)]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
← one_div,

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

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  ∀ (n_1 : ℕ),
    (coeff n_1) (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff n_1)
        (PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
simpa using

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  ∀ (n_1 : ℕ),
    (coeff n_1) (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff n_1)
        (PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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
⊢ ¬Nat.Prime x ∨ x ≤ n

Tactic:
simpa using

Goal state after:
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
⊢ ¬Nat.Prime x ∨ x ≤ n
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ.calc_4
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ C₁ + ∫ (t : ℝ) in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ ≤ C₁ + C₂

Tactic:
unfold C₂
        grw [setIntegral_mono_set ?_ (.of_forall fun _ ↦ norm_nonneg _)
          Set.Ioc_subset_Ioi_self.eventuallyLE]
        rw [← integrableOn_Ici_iff_integrableOn_Ioi, IntegrableOn,
          integrable_norm_iff (by fun_prop)]
        exact (locallyIntegrableOn_mul_sum_Icc _ m.cast_nonneg hf_int).integrableOn_of_isBigO_atTop
          hg₁ hg₂

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

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
⊢ Fintype.card (Fin M) * ?m.231 < Fintype.card (Fin (M ^ n.succ).succ)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
⊢ M * ?m.231 < (M * M ^ n).succ
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : abv.IsAdmissible
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h✝.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h✝.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h✝.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this : (M ^ n).succ ≤ {x | t x = s}.toList.length
i j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

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

Tactic:
simpa using

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
⊢ Fintype.card Fq ^ d ≤ m