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

Goal state before:
pp: case refine_1.refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
⊢ (closure L).toFun {m} ⊔ S ≤ f'.dom

Tactic:
simp only [sup_le_iff, ff'1, closure_le, singleton_subset_iff, SetLike.mem_coe, mf',
        and_self]

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
⊢ f = (f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)

Tactic:
ext ⟨x, hx⟩

Goal state after:
case refine_1.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
x : M
hx : x ∈ S
⊢ f ⟨x, hx⟩ = ((f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)) ⟨x, hx⟩
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})
x y : β
hx : ∃ a_1 < a, ∃ (x_1 : a_1 ∈ S), f ⟨a_1, ⋯⟩ = x
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
⊢ x < y

Tactic:
obtain ⟨_, hx, _, rfl⟩ := hx

Goal state after:
α : 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})
y : β
hy : ∃ a_1, a < a_1 ∧ ∃ (x : a_1 ∈ S), f ⟨a_1, ⋯⟩ = y
w✝¹ : α
hx : w✝¹ < a
w✝ : w✝¹ ∈ S
⊢ f ⟨w✝¹, ⋯⟩ < y
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
rw [age]

Goal state after:
M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ {N | FG Language.order ↑N ∧ Nonempty (↑N ↪[Language.order] M)} =
    {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
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
hG : IsGδ s
this✝¹ : LocallyCompactSpace ↑(closure s)
this✝ : BaireSpace ↑(closure s)
this : BaireSpace ↑(Subtype.val ⁻¹' s)
h_homeo : ↑(Subtype.val ⁻¹' s) ≃ₜ ↑s
⊢ BaireSpace ↑s

Tactic:
exact h_homeo.baireSpace

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
⊢ ∀ t₂ ∈ range T.typesWith, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range T.typesWith, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
t₂

Goal state after:
L : Language
T : L.Theory
α : Type u_1
t₁ : Set (T.CompleteType α)
φ : L[[α]].Sentence
ht₁ : T.typesWith φ = t₁
t₂ : Set (T.CompleteType α)
⊢ t₂ ∈ range T.typesWith → ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range T.typesWith, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
refine recOnPrimeCoprime ?_ ?_ ?_ n

Goal state after:
case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: case succ.h
R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
k : ℕ
ih : ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* R ⧸ span {↑p} := mk (span {↑p})
h : f a = f b
hf : ∀ (r : R), ↑p ∣ r ↔ f r = 0
⊢ ↑p = 0

Tactic:
rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) (pderivFun i ↑f) = (coeff n✝) ↑((pderiv i) f)

Tactic:
rw [coeff_pderivFun, coeff_coe, coeff_coe, coeff_pderiv]

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

Goal state before:
pp: hn : Odd 1
hn0 : 1 ≠ 0
⊢ Odd 3

Tactic:
by simp [Nat.odd_iff]

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

Goal state before:
pp: case hf
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‖ₑ)
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖⁻¹ • f x) μ

Tactic:
exact hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
⊢ (coeff n) (subst g ((d⁄dX R) ↑((trunc (m + 1)) f)) * (d⁄dX R) g) = (coeff n) (subst g ((d⁄dX R) f) * (d⁄dX R) g)

Tactic:
coeff_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
⊢ ∑ p ∈ Finset.antidiagonal n, (coeff p.1) (subst g ((d⁄dX R) ↑((trunc (m + 1)) f))) * (coeff p.2) ((d⁄dX R) g) =
    (coeff n) (subst g ((d⁄dX R) f) * (d⁄dX R) g)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ π (n - 1) = π' n

Tactic:
cases n <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ count Prime (k + n) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})

Tactic:
count_eq_card_filter_range,

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({x ∈ range (k + n) | Prime x}) ≤ #({p ∈ range k | Prime p}) + #({p ∈ Ico k (k + n) | Prime p})
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff (n + 1)) ((PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (exp A - 1)) =
    (coeff (n + 1)) (X * exp A)

Tactic:
coeff_mul,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ p ∈ antidiagonal (n + 1),
      (coeff p.1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) * (coeff p.2) (exp A - 1) =
    (coeff (n + 1)) (X * exp A)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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 ∈ ?m.256 ∧ p ≠ ?m.258

Tactic:
mem_sdiff,

Goal state after:
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 ∧ p ∉ {(1, n)}
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258
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)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
⊢ f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))

Tactic:
rw [log_div (mul_pos h5 h7).ne' (rpow_pos_of_pos four_pos _).ne', log_mul h5.ne' h7.ne',
      log_rpow h6, log_rpow zero_lt_four, ← mul_div_right_comm, ← mul_div, mul_comm x]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p =
    ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p

Tactic:
apply Finset.prod_subset

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

case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ ∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = ∑ n ∈ Icc 0 ⌊x⌋₊, Λ n

Tactic:
← add_sum_Ioc_eq_sum_Icc

Goal state after:
x : ℝ
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = Λ 0 + ∑ x ∈ Ioc 0 ⌊x⌋₊, Λ x

x : ℝ
⊢ 0 ≤ ⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0

Tactic:
← add_sum_Ioc_eq_sum_Icc

Goal state after:
x : ℝ
⊢ (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    (if Nat.Prime 0 then log ↑0 else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0

x : ℝ
⊢ 0 ≤ ⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

Tactic:
by
  simp_rw [lcmUpto_eq_prod_pow_log, ← natFloor_logb_natCast, ← log_div_log]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
⊢ ∃ x, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k

Tactic:
have hpn : p ≤ n := (le_of_dvd (by lia) (dvd_pow_self p hk.ne')).trans hx.2

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
hpn : p ≤ n
⊢ ∃ x, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mpr
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
i j : Fin (cardM bS adm).succ
hij : i ≠ j
⊢ ¬(distinctElems bS adm) i = (distinctElems bS adm) j

Tactic:
exact fun h => hij ((distinctElems bS adm).injective h)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ a ∈ Icc 1 N ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊),
      if
          match a with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
        match a with
        | (k, p) => f (p ^ k)
      else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
sum_product

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x_1 ∈ Icc 1 N,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (x_1, y) with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
          match (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n)) = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

Tactic:
← add_sum_Ioc_eq_sum_Icc

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ θ (x ^ (1 / ↑1)) + ∑ x_1 ∈ Ioc 1 N, θ (x ^ (1 / ↑x_1)) = θ x + ∑ n ∈ Icc 2 N, θ (x ^ (1 / ↑n))

x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ N
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ↑1 ≤ log x / log 2

Tactic:
le_div_iff₀ (by positivity),

Goal state after:
x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ↑1 * log 2 ≤ log x
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε

Tactic:
· refine ⟨Fin.cons j t', fun i₀ i₁ => ?_⟩
    refine Fin.cases ?_ (fun i₀ => ?_) i₀ <;> refine Fin.cases ?_ (fun i₁ => ?_) i₁
    · simpa using hbε
    · rw [Fin.cons_succ, Fin.cons_zero, eq_comm, AbsoluteValue.map_sub]
      exact hj i₁
    · rw [Fin.cons_succ, Fin.cons_zero]
      exact hj i₀
    · rw [Fin.cons_succ, Fin.cons_succ]
      exact ht' i₀ i₁

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
simpa only [Int.cast_natCast] using this

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.zmodRepr ≠ 0

Tactic:
rw [norm_natCast_zmodRepr_eq_one_iff, ne_eq, zmodRepr_eq_zero_iff_dvd, ← norm_lt_one_iff_dvd]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ = 1 ↔ ¬‖x‖ < 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)
x : (ZMod n)ˣ
⊢ (IsPrimitiveRoot.autToPow K ⋯) ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) =
    x

Tactic:
generalize_proofs _ h

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)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ (↑n).re = n

Tactic:
cases n <;> rfl

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

Goal state before:
pp: d n : ℤ
⊢ (↑n).im = 0

Tactic:
cases n <;> rfl

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

Goal state before:
pp: case inr.inl.inr.inr
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
exact nonneg_add_lem ha hb

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ (fun r ↦ { toFun := fun a ↦ ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((fun f ↦ ⟨f sqrtd, ⋯⟩) f) =
    f

Tactic:
by
    ext
    simp

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
⊢ Function.Surjective ⇑(domRestrictHom N R)

Tactic:
intro χ

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
⊢ ∃ a, (domRestrictHom N R) a = χ
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℤ
n : ℕ
⊢ (↑ξ).convergent n = ↑ξ

Tactic:
cases n
  · simp only [convergent_zero, floor_intCast]
  · simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero,
      inv_zero]

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

Goal state before:
pp: ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
⊢ False

Tactic:
cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2) <;> lia

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
this✝ : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
H : n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers

Tactic:
simp only [ne_eq, H, not_false_eq_true, true_and, or_not]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: case bot.bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
hy : ⊥ < ⊥
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < ⊥

Tactic:
simp at hy

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

Goal state before:
pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

Tactic:
rw [Nat.cast_one, div_one]

Goal state after:
case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
⊢ x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
(hx : 0 < x)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hC' : x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
hx : 0 < x
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖