mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ ¬IsField ↥(ringOfIntegers F K)

Tactic:
by
  simpa [← (IsIntegralClosure.isIntegral_algebra F[X] K).isField_iff_isField
      (algebraMap_injective F K)] using
    Polynomial.not_isField F

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ c x n ≤ b x (5 * n)

Tactic:
unfold c

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1) ≤ b x (5 * n)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_3
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
⊢ (algebraMap R S) M ∈ ↑↑⟨J, ⋯⟩

Tactic:
← Set.singleton_subset_iff,

Goal state after:
case refine_3
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
⊢ {(algebraMap R S) M} ⊆ ↑↑⟨J, ⋯⟩
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]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A

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]
t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 1 < x
⊢ log x ^ 2 ≠ 0

Tactic:
apply pow_ne_zero _ <| log_ne_zero.mpr ⟨_, _, _⟩ <;> linarith

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
conv => arg 2; ext; rw [← mul_one_div, mul_comm]

Goal state after:
case refine_2
⊢ (fun x ↦ 1 / log 2 ^ 2 * √x) =O[atTop] fun x ↦ x / log x ^ 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ log 4 * t / (t * log t ^ 2) = log 4 * (1 / log t ^ 2)

Tactic:
field

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 0 < x
⊢ (log x)⁻¹ = x / log x ^ 2 / (x / log x)

Tactic:
field

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
⊢ discr K = discr L

Tactic:
let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (f.restrictScalars ℤ).mapIntegralClosure.toLinearEquiv

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ discr K = discr L
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
rw [← B.basis.sum_repr z, Finset.smul_sum]

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
⊢ ∑ x, discr K ⇑B.basis • (B.basis.repr z) x • B.basis x ∈ R[B.gen]
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e'_2
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ⇑b = ⇑b' ᵥ* (b'.toMatrix ⇑b).map ⇑(algebraMap ℤ A)

pp: case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
· rw [Basis.toMatrix_map_vecMul]

Goal state after:
case e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'
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:
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.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
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)

Tactic:
have hpo : Odd p := hp.out.odd_of_ne_two hp2
      obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd
      rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos,
        Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow,
        pow_mul, hpo.pow.neg_one_pow]
      refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one
      rw [mul_left_comm, ← ha]
      exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.one_lt)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = b * { re := ↑a, im := -1 } * { re := ↑a, im := 1 }

Tactic:
rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp

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

Goal state before:
pp: case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
trivial

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
⊢ a ≤ b ∨ b ≤ a

Tactic:
have t := (b - a).nonneg_total
  rwa [neg_sub] at t

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
⊢ Nonneg 0

Tactic:
trivial

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑0, im := ↑0 } + { re := ofNat x, im := ofNat y }).Nonneg

Tactic:
trivial

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

Goal state before:
pp: case zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := 0, im := 0 }.Nonneg

Tactic:
trivial

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha : a.Nonneg
x y : ℕ
x✝ : { re := ↑x, im := ↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * ↑y }.Nonneg

Tactic:
trivial

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
⊢ 0 ≤ 1

Tactic:
trivial

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b c : ℤ√↑d
h : c + a ≤ c + b
⊢ a ≤ b

Tactic:
by
  exact _root_.le_of_add_le_add_left h

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

Goal state before:
pp: case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

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

Goal state before:
pp: case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ χ, χ a ≠ 1

Tactic:
refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
    refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
    contrapose ha
    rw [← hu.unit_spec, ha, Units.val_eq_one]

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

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite

Tactic:
refine Or.resolve_left (Set.finite_or_infinite _) fun h => ?_
  obtain ⟨q, _, hq⟩ :=
    exists_min_image {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2} (fun q => |ξ - q|) h
      ⟨⌊ξ⌋, by simp [abs_of_nonneg, Int.fract_lt_one]⟩
  obtain ⟨q', hmem, hbetter⟩ := exists_rat_abs_sub_lt_and_lt_of_irrational hξ q
  exact lt_irrefl _ (lt_of_le_of_lt (hq q' hmem) hbetter)

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

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |(↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num) / ↑ξ.den| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den

Tactic:
abs_div,

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| / |↑ξ.den| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
· obtain ⟨h₁, h₂⟩ :=
      abs_sub_lt_iff.mp
        (h.trans_le <|
          (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
    rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
    rw [← sub_lt_iff_lt_add] at h₂
    norm_cast at h₁ h₂
    exact
      ⟨sub_le_iff_le_add.mpr (Int.ceil_le.mpr h₁.le), sub_le_iff_le_add.mp (Int.le_floor.mpr h₂.le)⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ i, (χ * i) a = ∑ χ, χ a

Tactic:
exact Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl

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

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

Tactic:
field

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

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

Tactic:
abs_div,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ (↑v)⁻¹ ≤ |↑⌊ξ⌋ * ↑v - ↑u| / |↑v|
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Tactic:
exact mul_mem_factoredNumbers hm1 hm2

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u' = ↑u - ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹

Tactic:
rw [← hu'ℝ]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u' = ↑u - ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
⊢ (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v

Tactic:
field

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ ↑v / ↑u' - (fract ξ)⁻¹ = (fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)

Tactic:
field

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ (↑v * (2 * ↑v - 1))⁻¹ * (↑v / ↑u' / fract ξ) = (↑u' * ((2 * ↑v - 1) * fract ξ))⁻¹

Tactic:
field

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

Goal state before:
pp: case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ f n * ↑n ^ (-z)) (f n * (-log ↑n * ↑n ^ (-s))) s

Tactic:
exact HasDerivAt.const_mul (f n) (by simpa only [mul_comm, ← mul_neg_one (log n), ← mul_assoc]
    using (hasDerivAt_neg' s).const_cpow (Or.inl <| Nat.cast_ne_zero.mpr hn))

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

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < ↑(max x y) + 1
⊢ ↑(max x y) + 1 ∈ {s | x < s.re}

Tactic:
simp only [Set.mem_ofPred_eq, add_re, ofReal_re, one_re, hxy]

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

Goal state before:
pp: f : ℕ → ℂ
m : ℕ
⊢ abscissaOfAbsConv (logMul^[m] f) = abscissaOfAbsConv f

Tactic:
induction m with

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
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
⊢ (x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖) →
    x ∈ Ioi 0 → ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
hC'

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

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

Tactic:
field

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
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ mellin (fun x ↦ P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
calc
  _ = ∫ (x : ℝ) in Ioi 0, (x : ℂ) ^ (s - 1) •
      ((Ioo 0 1).indicator (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x
      + ({1} : Set ℝ).indicator (fun _ ↦ P.f₀ - P.f 1) x) :=
    setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ by simp [f_modif_aux1 P hx])
  _ = ∫ (x : ℝ) in Ioi 0, (x : ℂ) ^ (s - 1) • ((Ioo 0 1).indicator
      (fun t : ℝ ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x) := by
    refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))
    rw [indicator_of_notMem hx, add_zero]
  _ = ∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) := by
    simp_rw [← indicator_smul, setIntegral_indicator measurableSet_Ioo,
      inter_eq_right.mpr Ioo_subset_Ioi_self, integral_Ioc_eq_integral_Ioo]
  _ = ∫ x : ℝ in Ioc 0 1, ((x : ℂ) ^ (s - 1) • P.f₀ - P.ε • (x : ℂ) ^ (s - P.k - 1) • P.g₀) := by
    refine setIntegral_congr_fun measurableSet_Ioc (fun x ⟨hx, _⟩ ↦ ?_)
    rw [ofReal_cpow hx.le, ofReal_neg, smul_sub, ← mul_smul, mul_comm, mul_assoc, mul_smul,
      mul_comm, ← cpow_add _ _ (ofReal_ne_zero.mpr hx.ne'), ← sub_eq_add_neg, sub_right_comm]
  _ = (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - 1)) • P.f₀
        - P.ε • (∫ (x : ℝ) in Ioc 0 1, (x : ℂ) ^ (s - P.k - 1)) • P.g₀ := by
    rw [integral_sub, integral_smul, integral_smul_const, integral_smul_const]
    · apply Integrable.smul_const
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re1
    · refine (Integrable.smul_const ?_ _).smul _
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re2
  _ = _ := by
      simp_rw [← intervalIntegral.integral_of_le zero_le_one]
      match_scalars
      · simp [integral_cpow (.inl h_re1), zero_cpow (show s ≠ 0 by grind [P.hk, zero_re])]
      · simp [integral_cpow (.inl h_re2), zero_cpow (show s - P.k ≠ 0 by grind [P.hk, ofReal_re])]
        grind

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
⊢ ContinuousOn (fun p ↦ jacobiTheta₂' p.1 p.2) V

Tactic:
refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)

Goal state after:
case refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ ContinuousOn (fun p ↦ jacobiTheta₂'_term n p.1 p.2) V

case refine_2
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ'✝ : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
x✝¹ : ℂ × ℂ
z' τ' : ℂ
x✝ : (z', τ') ∈ V
hz' : (z', τ').1 ∈ {u | |u.im| < S}
hτ' : (z', τ').2 ∈ {v | T < v.im}
⊢ ‖jacobiTheta₂'_term n (z', τ').1 (z', τ').2‖ ≤ u n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Goal state after:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) =
    cexp (-(↑π * ↑a ^ 2 * ↑t) + (2 * ↑π * I * ↑n * (↑a * I * ↑t) + ↑π * I * ↑n ^ 2 * (I * ↑t)))