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

Goal state before:
pp: 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]‖ₑ + ↑δ
I5 : ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤ (μ.withDensity f B).variation s
⊢ ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s + ↑ε

Tactic:
calc ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation
  _ ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + δ := I1
  _ = ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) + δ := by rw [I2]
  _ ≤ (∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + δ) + δ := by gcongr
  _ ≤ ((∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + δ) + δ) + δ := by gcongr
  _ = (∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ) + 3 * δ := by ring
  _ ≤ (μ.withDensity f B).variation s + 3 * δ := by gcongr
  _ ≤ (μ.withDensity f B).variation s + ε := by
    simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, ENNReal.coe_div, ENNReal.coe_ofNat, δ]
    rw [ENNReal.mul_div_cancel (by simp) (by simp)]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]

Goal state after:
k m : ℕ
x✝ : m ∈ range (k + 1)
| (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m) * ↑(k + 1))
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ {p ∈ insert n (range n) | Prime p} = if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}

Tactic:
Finset.filter_insert

Goal state after:
n : ℕ
⊢ (if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}) =
    if Prime n then insert n ({p ∈ range n | Prime p}) else {p ∈ range n | Prime p}
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (d + 2) • (bernoulli (d + 1)).comp (1 + X) = (d + 2) • (bernoulli (d + 1) + (d + 1) • X ^ (d + 1 - 1))

Tactic:
← smul_comp,

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • bernoulli (d + 1)).comp (1 + X) = (d + 2) • (bernoulli (d + 1) + (d + 1) • X ^ (d + 1 - 1))
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
calc ((d + 2) • X ^ (d + 1)).comp (1 + X) - (d + 2) • X ^ (d + 1)
    _ = (d + 2) • ∑ i ∈ range (d + 1), (d + 1).choose i • X ^ i := by
      rw [smul_comp, ← smul_sub, X_pow_comp, one_add_X_pow_sub_X_pow]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose (i + 1) * (i + 1)) • X ^ i := by
      simp_rw [smul_sum, smul_smul, ← add_one_mul_choose_eq (d + 1)]
    _ = ∑ i ∈ range (d + 1), ((d + 2).choose i * i) • X ^ (i - 1) +
          (((d + 2).choose (d + 1)) * (d + 1)) • X ^ (d + 1 - 1) := by
      rw [← sum_range_succ _ (d + 1)]; simp [sum_range_succ']
    _ = ∑ i ∈ range (d + 1), (d + 2).choose i • i • X ^ (i - 1) +
          ((d + 2) * (d + 1)) • X ^ (d + 1 - 1) := by
      simp [choose_succ_self_right, add_assoc, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k
⊢ f ↑2 * c 2 + ∑ k ∈ Ioc ⌊2⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [sum_mul_eq_sub_sub_integral_mul c zero_le_two hb hf_diff hf_int]

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k
⊢ f ↑2 * c 2 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 2 * ∑ k ∈ Icc 0 ⌊2⌋₊, c k -
        ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
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_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.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
degree_eq_natDegree hb

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < ↑b.natDegree
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x y : ℝ
hxy : x ≤ y
⊢ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}

Tactic:
exact filter_subset_filter _ <| Ioc_subset_Ioc_right (by gcongr)

Goal state after:
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
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 < normBound abv bS

Tactic:
simp only [normBound, Algebra.smul_def, eq_natCast]

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
i j k : ι
hijk : (Algebra.leftMulMatrix bS) (bS i) j k ≠ 0
⊢ 0 <
    ↑(Fintype.card ι).factorial *
      (↑(Fintype.card ι) *
          (Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯) ^
        Fintype.card ι
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case mpr
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
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
⊢ e.symm.toRingEquiv c • x = c • x

Tactic:
convert! (this (e.symm c) x).symm

Goal state after:
case e'_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
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
b : Module.Basis (Fin (Module.finrank Ft K)) Ft K := Module.finBasis Ft K
c : Ft
x : K
⊢ c = e (e.symm c)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h.inl
x : ℝ
h : x ≤ 1
⊢ ψ x - θ x ≤ (log 4 + 4) * 3 * √x

Tactic:
theta_eq_zero_of_le_one h,

Goal state after:
case h.inl
x : ℝ
h : x ≤ 1
⊢ ψ x - 0 ≤ (log 4 + 4) * 3 * √x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ n % p = n

Tactic:
Nat.mod_eq_of_lt hn

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ n = 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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ Ideal.span {b} ≤ ↑I

Tactic:
rw [Ideal.span_le, Set.singleton_subset_iff]

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
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ b ∈ ↑↑I
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ Ideal.span {↑p}

Tactic:
by
      rw [← maximalIdeal_eq_span_p]
      exact sub_zmodRepr_mem

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

Goal state before:
pp: case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ Filter.Tendsto
    (⇑((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L)))) (nhds 1)
    (nhds 1)

Tactic:
(galGroupBasis K L).nhds_one_hasBasis.tendsto_iff
    (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))

Goal state after:
case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
⊢ ∀ (ib : ℝ),
    0 < ib →
      ∃ ia ∈ galGroupBasis K L,
        ∀ x ∈ id ia,
          ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
            Metric.ball 1 ib
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (toZModPow n) ((lift f_compat) r - ↑((f n) r).val) = 0

Tactic:
← RingHom.mem_ker,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (lift f_compat) r - ↑((f n) r).val ∈ RingHom.ker (toZModPow n)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case refine_3
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

Tactic:
exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

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

Goal state before:
pp: case refine_4
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

Tactic:
exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < a * a

Tactic:
rw [← this]

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
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
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    (Algebra.norm K) ((algebraMap K L) ↑(p ^ (k + 1))) * (Algebra.norm K) (ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
Algebra.norm_algebraMap,

Goal state after:
case e_a
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
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ (k + 1)) ^ Module.finrank K L * (Algebra.norm K) (ζ ^ (p ^ (k + 1) - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
t : { re := ↑a, im := 1 } ≤ { re := x, im := y } * ({ re := ↑a, im := -1 } * { re := ↑a, im := 1 })
⊢ False

Tactic:
Eq.trans (mul_comm _ _) a1m,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
t : { re := ↑a, im := 1 } ≤ { re := x, im := y } * 1
⊢ False
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
s : α ⊕ β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) s = (v ⊗ t) s

Tactic:
by rcases s with a | b <;> dsimp [(· ∘ ·)]; try rw [inv]; rfl

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

Goal state before:
pp: d : ℤ
n m : ℤ√d
⊢ (n * m).norm = n.norm * m.norm

Tactic:
simp only [norm, im_mul, re_mul]
  ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
rw [← this]

Goal state after:
case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n [MOD yn a1 n ^ 3]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ i ≤ 2 * n

Tactic:
apply le_trans hin

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ 2 * n
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ n ∈ {n | N ≤ n}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ N ≤ n
Module: Mathlib.NumberTheory.EulerProduct.ExpLog

Goal state before:
pp: f : ℕ →*₀ ℂ
hsum : Summable fun x ↦ ‖f x‖
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
by
  have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
  have hp (p : Nat.Primes) : 1 - f p ≠ 0 :=
    fun h ↦ (norm_one (α := ℂ) ▸ (sub_eq_zero.mp h) ▸ hs p.prop.one_lt).false
  have H := hsum.of_norm.clog_one_sub.neg.subtype Nat.Prime |>.hasSum.cexp.tprod_eq
  simp only [Function.comp_apply, exp_neg, exp_log (hp _)] at H
  exact H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t ↦ P.g (1 / t)) (↑P.k - s + -↑P.k)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ F_nat 0 0 t - 1 = F_nat 0 1 t

Tactic:
rw [F_nat, (summable_f_nat 0 0 ht).tsum_eq_zero_add, f_nat, Nat.cast_zero, add_zero, pow_zero,
      one_mul, pow_two, mul_zero, mul_zero, zero_mul, exp_zero, add_comm, add_sub_cancel_right]
    simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
⊢ HasSum (fun i ↦ s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))

Tactic:
simp_rw [← sq_eq_zero_iff (a := r _)] at hF

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
⊢ HasSum (fun i ↦ s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t)

Tactic:
← hasSum_ofReal,

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(rexp (-π * (↑x + a) ^ 2 * t))) ↑(evenKernel (↑a) t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) (cosKernel (↑a) t - 1)

Tactic:
← hasSum_ofReal,

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) ↑(cosKernel (↑a) t - 1)