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

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, Quotient.mk' x = ⟦a⟧) ↔ ∃ y, F y = ⟦a⟧
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K

Tactic:
simp_rw [Quotient.eq_mk_iff_out] at hF

Goal state after:
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
⊢ ∃ M, Structure.CG L ↑M ∧ L.age ↑M = K
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hl : p1 < a
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : a < p1
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b

Tactic:
· have : p1 < a ∧ p2 < b :=
      ⟨hl, hb.1 _ (Finset.mem_image.mpr ⟨(p1, p2), Finset.mem_filter.mpr ⟨hp, hl⟩, rfl⟩)⟩
    rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff] at this
    exact this.1.trans this.2.symm

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
this✝ : ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
b : β
hb : (∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), x < b) ∧ ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), b < y
p1 : α
p2 : β
hp : (p1, p2) ∈ ↑f
this : p1 ≠ a
hr : a < p1
⊢ cmp (p1, p2).1 a = cmp (p1, p2).2 b
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝ : L.IsOrdered
⊢ BoundedFormula.IsUniversal leSymb.reflexive ∧ BoundedFormula.IsUniversal leSymb.transitive

Tactic:
exact ⟨leSymb.isUniversal_reflexive, leSymb.isUniversal_transitive⟩

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

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

Tactic:
intro ⟨i, hi, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, hi, ?_⟩
      · apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
      · rw [mem_closure_singleton] at hy
        rcases hy with ⟨n, rfl⟩
        apply congr_arg (hs.floor · i) at heq
        rw [hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz,
          hs.floor_add_of_mem_closure sdiff_subset (notMem_sdiff_of_mem (mem_singleton i.1)) hz',
          add_assoc hs.base, ← succ_nsmul', hs.floor_add_nsmul_self, hs.floor_base, zero_add] at heq
        simp [heq]

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₂ : Set (T.CompleteType α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
⊢ x ∈ T.typesWith φ ∩ T.typesWith ψ ∧ T.typesWith φ ∩ T.typesWith ψ ⊆ t₁ ∩ t₂

Tactic:
ht₁,

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 α)
ψ : L[[α]].Sentence
ht₂ : T.typesWith ψ = t₂
x : T.CompleteType α
hx : x ∈ t₁ ∩ t₂
⊢ x ∈ t₁ ∩ T.typesWith ψ ∧ t₁ ∩ T.typesWith ψ ⊆ t₁ ∩ t₂
Module: Mathlib.NumberTheory.AlmostPrime

Goal state before:
pp: case mpr
n : ℕ
⊢ Prime n → IsAlmostPrime 1 n

Tactic:
· exact fun h ↦ ⟨h.ne_zero, ArithmeticFunction.cardFactors_eq_one_iff_prime.mpr h⟩

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: pqr : Multiset ℕ+
⊢ Admissible pqr → 1 < sumInv pqr

Tactic:
rw [Admissible]
  rintro (⟨p', q', H⟩ | ⟨n, H⟩ | H | H | H)
  · rw [← H, A', sumInv_pqr, add_assoc]
    simp only [lt_add_iff_pos_right, PNat.one_coe, inv_one, Nat.cast_one]
    apply add_pos <;> simp only [PNat.pos, Nat.cast_pos, inv_pos]
  · rw [← H, D', sumInv_pqr]
    norm_num
  all_goals
    rw [← H, E', sumInv_pqr]
    norm_num

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
⊢ λ a ∣ λ b

Tactic:
cases b
  · simp
  rw [carmichael_eq_exponent <| ne_zero_of_dvd_ne_zero (by lia) h, carmichael_eq_exponent']
  exact MonoidHom.exponent_dvd <| ZMod.unitsMap_surjective h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ λ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n.primeFactors.lcm fun p ↦ λ (p ^ n.factorization p)

Tactic:
exact carmichael_finsetProd pairwise_coprime_pow_primeFactors_factorization.set_of_subtype

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
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 ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p * (p.choose i / p)) =
    u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p)

Tactic:
simp only [Nat.cast_mul]

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
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (↑p * ↑(p.choose i / p)) =
    u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p)
Module: Mathlib.RingTheory.PowerSeries.Derivative

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

Tactic:
by
  induction n generalizing k with
  | zero => simp
  | succ n ih =>
    rw [Function.iterate_succ_apply', coeff_derivative, ih, Nat.ascFactorial_succ,
      ← Nat.succ_ascFactorial]
    grind

Goal state after:
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
⊢ IsCyclic (ZMod (2 * n))ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = x ^ x_1) ∨
      ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_two_mul_iff_of_odd _ hn, isCyclic_units_iff_of_odd hn, or_iff_right]
    · congr! with p m
      rw [Nat.mul_left_cancel_iff zero_lt_two, and_iff_right_of_imp]
      rintro rfl
      contrapose! h2
      cases Nat.lt_one_iff.mp h2
      rw [pow_zero, mul_one]
    · rintro ⟨p, m, -, odd, -, eq⟩
      have := eq ▸ odd.pow
      simp [← Nat.not_even_iff_odd] at this

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : 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⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ ∀ k ∈ Set.Ico ⌊a⌋₊.succ ⌊b⌋₊, IntervalIntegrable (fun t ↦ deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n) volume ↑k ↑(k + 1)

Tactic:
· exact fun k hk ↦ (intervalIntegrable_iff_integrableOn_Icc_of_le (mod_cast k.le_succ)).mpr
      <| (integrableOn_mul_sum_Icc c ha hf_int).mono_set
        <| (Set.Icc_subset_Icc_iff (mod_cast k.le_succ)).mpr <| mod_cast (ineqofmemIco hk)

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ π' k + #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ π' k + φ a * (n / a + 1)

Tactic:
add_le_add_iff_left

Goal state after:
a k : ℕ
h0 : a ≠ 0
h1 : a < k
n : ℕ
⊢ #({b ∈ Ico k (k + n) | a.Coprime b}) ≤ φ a * (n / a + 1)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ range (d + 1)
⊢ ((d + 2).choose x✝ • bernoulli x✝).comp (1 + X) = ?a.g x✝

Tactic:
· rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x

Tactic:
rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos, ←
    mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
    mul_one_div, ← log_nonpos_iff (hf' x h5).le, ← hf x h5]

Goal state after:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ f x ≤ 0
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
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 0 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k =
    ∑ k ∈ Icc 0 x✝, f ↑k * c k

Tactic:
sum_mul_eq_sub_integral_mul' _ _ (fun t ht ↦ hf_diff _ ht.1)

Goal state after:
𝕜 : 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
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 0 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k =
    f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 0 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

𝕜 : 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
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 0 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ IntegrableOn (deriv f) (Set.Icc 0 ↑x✝) volume
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
hv : M.factorization p ≤ N
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
by
  set e := M.factorization p
  set M' := M / p ^ e
  have hM'_cop : M'.Coprime p := (Nat.coprime_ordCompl Fact.out hM).symm
  have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)
  -- Rewrite p^N / M as p^(N-e) / M' where M' = M / p^e is coprime to p
  have hdecomp : p ^ e * M' = M := Nat.ordProj_mul_ordCompl_eq_self M p
  have hM_eq : (M : ℚ) = ↑(p ^ e) * ↑M' := by rw [← hdecomp]; simp
  have hrw : (p : ℚ) ^ N / M = (p : ℚ) ^ (N - e) / M' := by
    rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]
    congr 1
    rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
  have hM'_eq : ((p : ℚ) ^ (N - e) / (M' : ℚ)) = Rat.divInt (p ^ (N - e) : ℤ) (M' : ℤ) := by
    norm_cast
    simp
  rw [hrw]
  exact Rat.padicValuation_le_one_iff.2 ((Nat.Prime.coprime_iff_not_dvd Fact.out).1
    (hM'_cop.coprime_dvd_left (by
      rw [hM'_eq]; exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _))).symm)

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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
⊢ 0 < cardPowDegree b • ε

Tactic:
rw [Algebra.smul_def, eq_intCast]

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x ≤ ↑(π ⌊x⌋₊) * log x

Tactic:
psi_eq_psi_coe_floor,

Goal state after:
x : ℝ
⊢ ψ ↑⌊x⌋₊ ≤ ↑(π ⌊x⌋₊) * log x
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < cardPowDegree b • ε

Tactic:
rw [Algebra.smul_def, eq_intCast]

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
⊢ bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
have hT : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) + vonStaudtIndicator (2 * k) p =
      p * T := by unfold vonStaudtIndicator; exact_mod_cast hT_int

Goal state after:
case h
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
⊢ bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
psi_eq_psi_coe_floor,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ ↑⌊x⌋₊
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
grw [psi_eq_psi_coe_floor, ← psi_ge]

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ↑⌊x⌋₊ * log 2 - log (↑⌊x⌋₊ + 1)
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ (fun c ↦ (algebraMap Ft K) (e c)) = ⇑(algebraMap F⟮X⟯ K)

Tactic:
refine IsLocalization.ext (nonZeroDivisors F[X]) _ _ ?_ ?_ ?_ ?_ ?_

Goal state after:
case e_a.refine_1
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ (algebraMap Ft K) (e 1) = 1

case e_a.refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ (algebraMap F⟮X⟯ K) 1 = 1

case e_a.refine_3
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ ∀ (a b : F⟮X⟯), (algebraMap Ft K) (e (a * b)) = (algebraMap Ft K) (e a) * (algebraMap Ft K) (e b)

case e_a.refine_4
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ ∀ (a b : F⟮X⟯), (algebraMap F⟮X⟯ K) (a * b) = (algebraMap F⟮X⟯ K) a * (algebraMap F⟮X⟯ K) b

case e_a.refine_5
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ ∀ (a : F[X]), (algebraMap Ft K) (e ((algebraMap F[X] F⟮X⟯) a)) = (algebraMap F⟮X⟯ K) ((algebraMap F[X] F⟮X⟯) a)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
obtain ⟨N₅, h5⟩ := psi_pow_eq_sum_b x 5 hx

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
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:
by
  rw [norm_natCast_zmodRepr_eq_one_iff, ne_eq, zmodRepr_eq_zero_iff_dvd, ← norm_lt_one_iff_dvd]
  simp

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
⊢ DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) z

Tactic:
have : z ≠ 0 := by linarith

Goal state after:
case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) z
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
⊢ ContinuousWithinAt (fun x ↦ -x⁻¹ / log x ^ 2) (Set.Icc 2 x) z

Tactic:
have : z ≠ 0 := by linarith

Goal state after:
case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ ContinuousWithinAt (fun x ↦ -x⁻¹ / log x ^ 2) (Set.Icc 2 x) z
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ toZMod x = 0 → x ∈ maximalIdeal ℤ_[p]

Tactic:
intro h
    simpa only [h, ZMod.cast_zero, sub_zero] using toZMod_spec x

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ θ x = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
rw [theta_eq_sum_Icc, sum_filter]
  let a : ℕ → ℝ := Set.indicator (Set.ofPred Nat.Prime) (fun n ↦ 1)
  trans ∑ n ∈ Icc 0 ⌊x⌋₊, log n * a n
  · refine sum_congr rfl fun n _ ↦ ?_
    split_ifs with h <;> simp [a, h]
  rw [sum_mul_eq_sub_integral_mul₁ a (by simp [a, not_prime_zero])
    (by simp [a, not_prime_one]) _ (fun z ⟨hz, _⟩ ↦ (by fun_prop (disch := linarith))) ?hint,
    ← intervalIntegral.integral_of_le hx]
  case hint =>
    rw [deriv_log']
    refine ContinuousOn.integrableOn_Icc ?_
    fun_prop (disch := grind)
  -- Rewrite the derivative inside the integral
  simp only [primeCounting, primeCounting', count_eq_card_filter_range]
  have int_deriv (f : ℝ → ℝ) :
      ∫ u in 2..x, deriv (fun x ↦ log x) u * f u =
      ∫ u in 2..x, f u / u :=
    intervalIntegral.integral_congr fun u _ ↦ by rw [deriv_log, mul_comm, div_eq_mul_inv]
  rw [int_deriv]
  simp [a, Set.indicator_apply, range_succ_eq_Icc_zero, mul_comm]

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

Goal state before:
pp: case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ ∀ (x : ℤ_[p]), ↑p ^ 0 ∣ x - ↑(x.appr 0)

Tactic:
simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖

Tactic:
integral_one_div_log_sq_le_explicit hx,

Goal state after:
x : ℝ
hx : 4 ≤ x
⊢ 4 * x / log x ^ 2 + √x / log 2 ^ 2 ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0

Tactic:
by
  obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
  have : (traceMatrix A b) *ᵥ g = 0 := by
    ext i
    have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by
      intro j
      simp [mul_comm]
    simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j =>
      this j, ← map_sum, ← sum_mul, hg, zero_mul, map_zero]
  by_contra h
  rw [discr_def] at h
  simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi

Goal state after: