mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr
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‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
I4 :
  ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ
Q : Finset (Set X) := Finset.image (fun p ↦ p.snd ∩ s) (g.range.sigma P)
i : E
p : Set X
j : E
q : Set X
hijpq : ⟨i, p⟩ ≠ ⟨j, q⟩
h'ij : ⟨i, p⟩.snd ∩ s = ⟨j, q⟩.snd ∩ s
hi : (∃ y, g y = i) ∧ p ∈ P i
hj : (∃ y, g y = j) ∧ q ∈ P j
hij : i ≠ j
⊢ Disjoint p q

Tactic:
have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind
          exact this.mono (Pg i p hi.2) (Pg j q hj.2)

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + (↑↑p')⁻¹ + (↑↑q')⁻¹

Tactic:
add_assoc

Goal state after:
case inl
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 1 < (↑↑1)⁻¹ + ((↑↑p')⁻¹ + (↑↑q')⁻¹)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) = (λ a).lcm (λ b)

Tactic:
apply dvd_antisymm

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ λ (a.lcm b) ∣ (λ a).lcm (λ b)

case a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ (λ a).lcm (λ b) ∣ λ (a.lcm b)
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) =
    ↑p * u * (v * (a * x ^ 2 * ((u * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
rw [ha]; ring

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

Goal state before:
pp: case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(↑(p ^ (n + m)) * a) = 0

Tactic:
ZMod.intCast_zmod_eq_zero_iff_dvd,

Goal state after:
case refine_2.hnot
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(p ^ (n + 1 + m)) ∣ ↑(p ^ (n + m)) * a
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
f g : MvPowerSeries σ R
⊢ pderivFun i (f + g) = pderivFun i f + pderivFun i g

Tactic:
ext
  rw [coeff_pderivFun, map_add, map_add, coeff_pderivFun, coeff_pderivFun, add_mul]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1)) ↑((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))

Tactic:
coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f * (pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))

Tactic:
coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g * (pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))

Tactic:
coe_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((pderiv i) ((trunc R (n + single i 1 + single i 1)) g)) +
        ↑((trunc R (n + single i 1 + single i 1)) g) * ↑((pderiv i) ((trunc R (n + single i 1 + single i 1)) f)))
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
⊢ (coeff n) f = (coeff n) g

Tactic:
have e := congr(coeff (n - single i 1) $(hD i))

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 - single i 1)) ((pderiv R i) f) = (coeff (n - single i 1)) ((pderiv R i) g)
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
or_iff_left

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1

case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n i : ℕ
⊢ (bernoulli n).coeff i = if i ≤ n then _root_.bernoulli (n - i) * ↑(n.choose i) else 0

Tactic:
simp only [bernoulli, finsetSum_coeff, coeff_monomial]
  split_ifs with h
  · convert! sum_ite_eq_of_mem (range (n + 1)) (n - i) _ (by grind) using 3 <;> grind [choose_symm]
  · exact Finset.sum_eq_zero <| by grind

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) 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
⊢ Tendsto (fun n ↦ ∑ k ∈ Icc 0 n, f ↑k * c k) atTop (𝓝 (l - ∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))

Tactic:
by
  have h : (fun n : ℕ ↦ ∫ (x : ℝ) in (1 : ℝ)..n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop]
      (fun n : ℕ ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) := by
    filter_upwards [eventually_ge_atTop 1] with _ h
    rw [← integral_of_le (Nat.one_le_cast.mpr h)]
  have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (1 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
      atTop (𝓝 (∫ t in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
    refine Tendsto.congr' h (intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop)
    exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c zero_le_one hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int
  refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
  rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]
  exact hf_int.integrableOn_compact_subset Set.Icc_subset_Ici_self isCompact_Icc

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

Goal state before:
pp: case h
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) < ↑|b|

Tactic:
cast_lt

Goal state after:
case h
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < ⊥
⊢ False

Tactic:
exact not_lt_of_ge bot_le hA

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : θ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
⊢ False

Tactic:
have h₁ : log (↑(2 : ℕ) : ℝ) ≤ θ x :=
    single_le_sum (fun p hp ↦ log_nonneg (by aesop)) (by aesop (add simp prime_two))

Goal state after:
x : ℝ
h₀ : θ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
h₁ : log ↑2 ≤ θ x
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = log ↑(primorial ⌊x⌋₊)

Tactic:
unfold theta primorial
  rw [cast_prod, log_prod (fun p hp ↦ mod_cast (mem_filter.mp hp).2.pos.ne')]
  congr 1 with p
  simp_all [Prime.pos]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ ((Icc 1 n).sup fun a ↦ (id a).factorization p) = log p n

Tactic:
have := hp.one_lt

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

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

Tactic:
grw [psi_eq_psi_coe_floor, psi_le_primeCounting_mul_log]

Goal state after:
x : ℝ
⊢ ↑(π ⌊x⌋₊) * log ↑⌊x⌋₊ ≤ ↑(π ⌊x⌋₊) * log x
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]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < log (cardPowDegree b • ε)

Tactic:
cardPowDegree_nonzero _ h',

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]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(A i₁ % b - A i₀ % b).natDegree < ↑b.natDegree + log ε / log ↑(Fintype.card Fq)
⊢ log ↑(↑(Fintype.card Fq) ^ (A i₁ % b - A i₀ % b).natDegree) < log (cardPowDegree b • ε)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ∈ Set.Ici 1
m : ℕ
hm : m ∈ Set.Ici 1
⊢ n ≤ m → b x m ≤ b x n

Tactic:
hnm

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
hn : n ∈ Set.Ici 1
m : ℕ
hm : m ∈ Set.Ici 1
hnm : n ≤ m
⊢ b x m ≤ b x n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, 1 / ↑q).den

Tactic:
by
  rw [sum_one_div_prime_eq_indicator_div_add (p := p) hk, ← add_assoc]
  have hcop_ind := ((Nat.Prime.coprime_iff_not_dvd Fact.out).mpr
    (not_dvd_den_bernoulli_add_indicator (p := p) hk)).symm
  have hcop_rest := Nat.Coprime.of_dvd_left (Rat.den_sum_dvd_prod_den _ _)
    (prod_one_div_prime_den_coprime k (p := p))
  have hcop := (Nat.Coprime.of_dvd_left (Rat.add_den_dvd _ _) (hcop_ind.mul_left hcop_rest)).symm
  exact (Nat.Prime.coprime_iff_not_dvd Fact.out).1 hcop

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑(a - b) = 0

Tactic:
ZMod.intCast_zmod_eq_zero_iff_dvd,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑(p ^ n) ∣ a - b
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_2.refine_2
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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₀.succ % b)) <
    cardPowDegree b • ε
⊢ False

Tactic:
· rw [Fin.cons_succ, Fin.cons_succ] at approx
      rw [Ne, Fin.succ_inj] at j_ne
      have : j₀ = j₁ := (Classical.choose_spec (hg j₀)).1.symm.trans
        (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
          (Classical.choose_spec (hg j₁)).1)
      contradiction

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ x.appr n - x.appr m

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h; clear h
  induction k with
  | zero =>
    simp only [add_zero, le_refl, tsub_eq_zero_of_le, dvd_zero]
  | succ k ih =>
    rw [← add_assoc]
    dsimp [appr]
    split_ifs with h
    · exact ih
    rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
    apply dvd_add _ ih
    apply dvd_mul_of_dvd_left
    apply pow_dvd_pow _ (Nat.le_add_right m k)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:

Tactic:
|∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
        intervalIntegral.abs_integral_le_integral_abs (by linarith)
    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity

Goal state after:
case hf
x : ℝ
a✝ : 4 ≤ x
⊢ IntervalIntegrable (fun x ↦ |θ x / (x * log x ^ 2)|) volume 2 x

case hg
x : ℝ
a✝ : 4 ≤ x
⊢ IntervalIntegrable (fun x ↦ log 4 * (1 / log x ^ 2)) volume 2 x

case hh
x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ |θ t / (t * log t ^ 2)| ≤ log 4 * (1 / log t ^ 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log ↑p + if ↑p ≤ √x then log √x else 0) ≤ log 4 * x + √x * log √x

Tactic:
grw [← theta_le_log4_mul_x (by positivity)]

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log ↑p + if ↑p ≤ √x then log √x else 0) ≤ θ x + √x * log √x
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
⊢ Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)

Tactic:
exact Fintype.card_congr e.symm

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case f
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : L →ₐ[K] E
| eval (σ pb.gen) (derivative (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))

Tactic:
(IsAlgClosed.splits _).eval_root_derivative ((minpoly.monic pb.isIntegral_gen).map _)
      (hroots σ),

Goal state after:
case f
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : L →ₐ[K] E
| (Multiset.map (fun x ↦ σ pb.gen - x)
      ((Polynomial.map (algebraMap K E) (minpoly K pb.gen)).roots.erase (σ pb.gen))).prod
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b = discr ℤ ⇑b'

Tactic:
by
  convert! Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)
  · rw [Basis.toMatrix_map_vecMul]
  · suffices IsUnit (b'.toMatrix b).det by
      rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
      rw [this, one_mul]
    rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']
    exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ ↑n ≤ pellZd a1 n

Tactic:
rw [Zsqrtd.natCast_val]
      exact
        Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
          (Int.natCast_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
this :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } =
    { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
injection this with h₁ h₂

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + 2 * n + j) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
add_assoc

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)

Tactic:
try { cases a <;> rfl }

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a ^ Nat.card (ZMod n)ˣ‖ = 1

Tactic:
← map_pow,

Goal state after:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ (↑a ^ Nat.card (ZMod n)ˣ)‖ = 1