mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ
⊢ (μ.withDensityᵥ f).variation = μ.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
rcases subsingleton_or_nontrivial E with hE | hE
  · simp [show f = 0 from Subsingleton.elim _ _]
  have : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ) := ⟨by simpa using! hf.2⟩
  have I : (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure.Integrable (fun x ↦ ‖f x‖⁻¹ • f x) := by
    simp only [VectorMeasure.Integrable, Measure.variation_toSignedMeasure]
    apply Integrable.of_bound (C := 1)
    · apply AEStronglyMeasurable.mono_ac (withDensity_absolutelyContinuous _ _)
      exact hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable
    · filter_upwards with x using by simp [norm_smul, inv_mul_le_one]
  have : μ.withDensityᵥ f = (μ.withDensity (‖f ·‖ₑ)).toSignedMeasure.withDensity
      (fun x ↦ ‖f x‖⁻¹ • f x) (ContinuousLinearMap.lsmul ℝ ℝ).flip := by
    ext s hs
    rw [withDensityᵥ_apply hf hs, withDensity_apply I, setIntegral_toSignedMeasure hs,
        setIntegral_withDensity_eq_setIntegral_toReal_smul₀ _ _ _ hs]; rotate_left
    · exact hf.aestronglyMeasurable.restrict.enorm
    · filter_upwards with x using by simp
    congr with x
    rcases eq_or_ne (f x) 0 with hx | hx
    · simp [hx]
    simp only [toReal_enorm, smul_smul]
    rw [mul_inv_cancel₀, one_smul]
    simpa using hx
  rw [this, variation_withDensity I (by simp [nnnorm_smul, mul_comm]),
    variation_transpose_eq _ _ (by simp [nnnorm_smul, mul_comm]), Measure.variation_toSignedMeasure,
    ← withDensity_mul₀ hf.aestronglyMeasurable.enorm]; swap
  · exact (hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable).enorm
  congr with x
  rcases eq_or_ne (f x) 0 with hx | hx
  · simp [hx]
  have h'x : ‖f x‖ ≠ 0 := by simp [hx]
  simp only [enorm_smul, Pi.mul_apply, ne_eq, h'x, not_false_eq_true, enorm_inv, enorm_norm]
  rw [ENNReal.inv_mul_cancel (by simpa using hx) (by simp), mul_one]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
| ∑ x ∈ range (n + 1 - 0),
    ∑ x_1 ∈ range (n + 1 - x), (monomial x) (↑((n + 1).choose (x + x_1)) * ↑((x + x_1).choose x) * _root_.bernoulli x_1)

Tactic:
apply_congr

Goal state after:
case h
n : ℕ
⊢ range (n + 1 - 0) = ?s₂

case a
n x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ ∑ x ∈ range (n + 1 - x✝), (monomial x✝) (↑((n + 1).choose (x✝ + x)) * ↑((x✝ + x).choose x✝) * _root_.bernoulli x) =
    ?g x✝
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - 0)
| ∑ x ∈ range (n + 1 - x✝), (monomial x✝) (↑((n + 1).choose (x✝ + x)) * ↑((x✝ + x).choose x✝) * _root_.bernoulli x)

Tactic:
apply_congr

Goal state after:
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - 0)
⊢ range (n + 1 - x✝) = ?s₂

case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1 - 0)
x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ (monomial x✝¹) (↑((n + 1).choose (x✝¹ + x✝)) * ↑((x✝¹ + x✝).choose x✝¹) * _root_.bernoulli x✝) = ?g x✝
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (1 + X)

Tactic:
apply_congr

Goal state after:
case a.h
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ range (d + 1) = ?a.s₂

case a.a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
x✝ : ℕ
a✝ : x✝ ∈ ?a.s₂
⊢ ((d + 2).choose x✝ • bernoulli x✝).comp (1 + X) = ?a.g x✝
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (coeff n) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff n) (X * exp A)

Tactic:
cases n with | zero => simp | succ n =>
  rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
  suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
  apply eq_inv_of_mul_eq_one_left
  rw [sum_mul]
  convert! bernoulli'_spec' n using 1
  apply sum_congr rfl
  simp_rw [mem_antidiagonal]
  rintro ⟨i, j⟩ rfl
  have := factorial_mul_factorial_dvd_factorial_add i j
  simp [field, add_choose, *]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n : ℕ
⊢ (bernoulli (n + 1)).comp (-X) = (-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))

Tactic:
ext i

Goal state after:
case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-X)).coeff i = ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i
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 +decide [Nat.factorial] using h 1

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)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
⊢ f x = log (x * (2 * x) ^ √(2 * x)) - log (4 ^ (x / 3))

Tactic:
log_mul h5.ne' h7.ne',

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)
x : ℝ
h5 : 0 < x
h6 : 0 < 2 * x
h7 : 0 < (2 * x) ^ √(2 * x)
⊢ f x = log x + log ((2 * x) ^ √(2 * x)) - log (4 ^ (x / 3))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
mul_left_comm,

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ (algebraMap ℚ A) ↑(n + 1)! *
      ∑ x ∈ range (n + 1),
        (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
          ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * ((algebraMap ℚ A) ↑(n + 1)! * (algebraMap ℚ A) (1 / ↑n !))
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_1
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
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 18) = 6
⊢ 1 ≤ 18 * (2 * 18) ^ 6 / 4 ^ (18 / 3)

Tactic:
one_le_div (by norm_num1)

Goal state after:
case refine_1
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
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 18) = 6
⊢ 4 ^ (18 / 3) ≤ 18 * (2 * 18) ^ 6
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i

Tactic:
by simp_rw [sum_range_succ']

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

Goal state before:
pp: case succ.refine_2
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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i✝ : Fin (n + 1)
i : Fin n
⊢ ↑(abv (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) < abv b • ε

Tactic:
exact h i

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
⊢ (d + 1).factorization p ≤ d - 1

Tactic:
by
  by_cases hcase : p = 2 ∧ d = 2
  · obtain ⟨rfl, rfl⟩ := hcase
    simp [Nat.factorization_eq_zero_of_not_dvd (by decide : ¬(2 ∣ 3))]
  · apply Nat.factorization_le_of_le_pow
    have hp2 := (Fact.out : p.Prime).two_le
    suffices ∀ n : ℕ, n ≥ 2 → ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1) from this d hd hcase
    intro n hn hne'
    induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ 2 * ↑k - 2 * ↑m + 1 ≠ 0

Tactic:
by norm_cast; lia

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ↑((2 * k + 1).choose (2 * m)) * ↑(2 * k + 1 - 2 * m) = ↑((2 * k).choose (2 * m)) * (2 * ↑k + 1)

Tactic:
exact_mod_cast Nat.choose_mul_succ_eq (2 * k) (2 * m) |>.symm

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∏ p ∈ range (n + 1) with Prime p, p ∣ n.lcmUpto

Tactic:
rw [← primesLE_eq_filter_range, ← primeFactors_lcmUpto]

Goal state after:
n : ℕ
⊢ ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ primorial n ∣ n.lcmUpto

Tactic:
simp only [primorial]
  rw [← primesLE_eq_filter_range, ← primeFactors_lcmUpto]
  exact prod_primeFactors_dvd _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ #n.primesLE • log ↑n

Tactic:
← sum_const

Goal state after:
n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n = log (∏ i ∈ n.primesLE, ↑(i ^ Nat.log i n))

Tactic:
log_prod (by simp +contextual)

Goal state after:
n : ℕ
⊢ ψ ↑n = ∑ i ∈ n.primesLE, log ↑(i ^ Nat.log i n)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
have s_eq : ∀ i, s i = bS.repr a i := fun i => rfl

Goal state after:
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0

Tactic:
· exact mod_cast hp_prime.1.ne_zero

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

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)

Tactic:
calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_

Goal state after:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ n + p ^ n * (p - 1)

case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: 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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
r' : S
hr' : (algebraMap R S) M ∣ r'
a : S
ha : a ∈ ↑I
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt : abv ((Algebra.norm R) ((algebraMap R S) r * a - q * b)) < abv ((Algebra.norm R) b)
⊢ r ∣ M

Tactic:
exact Multiset.dvd_prod (Multiset.mem_map.mpr ⟨_, r_mem, rfl⟩)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2) =o[atTop] fun x ↦ x / √x

pp: ⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0

Tactic:
· simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]
      apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
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
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ traceMatrix A b *ᵥ g = 0

Tactic:
ext i

Goal state after:
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
g : ι → A
hg : ∑ i, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ (traceMatrix A b *ᵥ g) i = 0 i
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_f
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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (fun x ↦ (∏ j > x, ((e j) pb.gen - (e x) pb.gen)) ^ 2) = fun i ↦ ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
ext i

Goal state after:
case e_f
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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
i : Fin pb.dim
⊢ (∏ j > i, ((e j) pb.gen - (e i) pb.gen)) ^ 2 = ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_f
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)
⊢ (fun i ↦ ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun i ↦
    ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
ext i

Goal state after:
case e_f
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)
i : Fin pb.dim
⊢ ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2 = ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

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

Tactic:
mul_left_comm,

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

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

Tactic:
mul_left_comm,

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

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ n * a ≤ xn a1 n * a + d a1 * yn a1 n

Tactic:
exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n - ↑(d a1) * yz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg]
  exact congr_arg Zsqrtd.re (pellZd_sub a1 h)

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ (fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm = fun i ↦ (algebraMap K L) (-1) ^ ↑i

Tactic:
ext i

Goal state after:
case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ((fun i ↦ (algebraMap K L) (-1) ^ ↑i) ∘ ⇑e.symm) i = (algebraMap K L) (-1) ^ ↑i
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ 2 * n - j + j ≤ n + j

Tactic:
tsub_add_cancel_of_le h,

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ 2 * n ≤ n + j
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ.toUnitHom a = 1
⊢ χ ↑a = 1

Tactic:
rwa [Units.ext_iff, coe_toUnitHom] at hχ

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

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|

Tactic:
have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)

Goal state after:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ ↑a.num / ↑a.den = b

Tactic:
← Rat.num_div_den b,

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ ↑a.num / ↑a.den = ↑b.num / ↑b.den
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: v : ℤ
hv : 0 < v
⊢ 0 < 2 * ↑v - 1

Tactic:
by norm_cast; lia

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

Goal state before:
pp: case bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ⊥

Tactic:
refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_

Goal state after:
case bot
f : ℕ → ℂ
h : ∀ (y : ℝ), ⊥ < ↑y → LSeriesSummable f ↑y
y : EReal
hy : ⊥ < y
⊢ ∃ a ∈ Real.toEReal '' {x | LSeriesSummable f ↑x}, a < y
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)

Tactic:
by
  rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _

Goal state after: