mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [degree_eq_natDegree hb] at hbj

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.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: 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
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ j = b.natDegree - (b.natDegree - j)

Tactic:
tsub_tsub_cancel_of_le hbj.le

Goal state after:
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
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ j = j
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

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

Tactic:
eq_intCast

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

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

Tactic:
eq_intCast

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑(cardPowDegree b) * ε
Module: Mathlib.NumberTheory.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
⊢ FunctionField F K

Tactic:
let b := Module.finBasis Ft K

Goal state after:
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
⊢ FunctionField F K
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁✝ : Fin (n + 1)
i₀ i₁ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' i₁.succ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε

Tactic:
· rw [Fin.cons_succ, Fin.cons_succ]
      exact ht' i₀ i₁

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

Goal state before:
pp: case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ 1 - ↑1 ∈ Ideal.span {↑v}

Tactic:
simp only [sub_self, cast_one, Submodule.zero_mem]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x / log x ^ 2 / (x / log x)) atTop (nhds 0)

Tactic:
refine Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop

Goal state after:
⊢ (fun x ↦ (log x)⁻¹) =ᶠ[atTop] fun x ↦ x / log x ^ 2 / (x / log x)
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
primeCounting_eq_theta_div_log_add_integral hx

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) = (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) - θ x / log x
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ c.val = ↑t ^ ((ZMod.ringEquivCongr ⋯) c).val

Tactic:
ZMod.ringEquivCongr_val

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ c.val = ↑t ^ c.val
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
r : R
i j : ℕ
h : i ≤ j
⊢ ↑p ^ i ∣ nthHom f r j - nthHom f r i

Tactic:
by
  specialize f_compat i j h
  rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]
  dsimp [nthHom]
  rw [← f_compat, RingHom.comp_apply]
  simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.natCast_val, ZMod.intCast_cast]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']
    apply xn_modEq_x2n_add

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case cons
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) (S :: l) ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl

Tactic:
| cons S l IH =>

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:
pow_card_eq_one',

Goal state after:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑1‖ = 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case zero
ξ : ℤ
⊢ (↑ξ).convergent 0 = ↑ξ

Tactic:
simp only [convergent_zero, floor_intCast]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1

Tactic:
have w1 : 1 < w + 1 := Nat.succ_lt_succ wpos

Goal state after:
case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := max n k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ↑⌊ξ⌋
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
hξ₁,

Goal state after:
case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ↑(u - 1)
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
m : ℕ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
⊢ iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s

Tactic:
by
  induction m generalizing s with
  | zero => simp
  | succ m ih =>
    have ih' : {s | abscissaOfAbsConv f < re s}.EqOn (iteratedDeriv m (LSeries f))
        ((-1) ^ m * LSeries (logMul^[m] f)) := fun _ hs ↦ ih hs
    have := derivWithin_congr ih' (ih h)
    simp_rw [derivWithin_of_isOpen (isOpen_re_gt_EReal _) h] at this
    rw [iteratedDeriv_succ, this]
    simp [Pi.mul_def, pow_succ, Function.iterate_succ',
      LSeries_deriv <| absicssaOfAbsConv_logPowMul.symm ▸ h, -Function.iterate_succ]

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

Goal state before:
pp: ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ 2⁻¹ < ξ - ↑⌊ξ⌋

Tactic:
hξ₁,

Goal state after:
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ 2⁻¹ < ξ - ↑(u - 1)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inl
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
⊢ Tendsto (fun n ↦ ↑n * (-π * τ.im) - 2 * π * z.im) atTop atTop

Tactic:
exact tendsto_atTop_add_const_right _ _ (tendsto_natCast_atTop_atTop.atTop_mul_const
        (mul_pos_of_neg_of_neg (neg_lt_zero.mpr pi_pos) hτ))

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

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ F_int k (↑a) t = F_nat k a t + F_nat k (1 - a) t

Tactic:
by
  simp only [F_int, F_nat, Function.Periodic.lift_coe]
  convert!
    ((summable_f_nat k a ht).hasSum.int_rec (summable_f_nat k (1 - a) ht).hasSum).tsum_eq using
    3 with n
  cases n
  · rw [f_int_ofNat _ ha.1]
  · rw [f_int_negSucc _ ha.2]

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

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
jacobiTheta₂_undef _ hτ,

Goal state after:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * 0)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ Tendsto (fun s ↦ (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (𝓝[>] 1) (𝓝 1)

Tactic:
← tendsto_ofReal_iff,

Goal state after:
⊢ Tendsto (fun x ↦ ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 ↑1)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (n : ↑({p | Nat.Prime p} ∩ {p | k ≤ p})), {p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False

Tactic:
tsum_subtype,

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk :
  ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n) x ∈ Iio (1 / 2)
⊢ False
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
⊢ False

Tactic:
have h' : Summable (indicator ({p | Nat.Prime p} ∩ {p | k ≤ p}) fun n ↦ (1 : ℝ) / n) := by
    convert! h.indicator {n : ℕ | k ≤ n} using 1
    simp only [indicator_indicator, inter_comm]

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
have : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / Gammaℝ s) (𝓝[≠] 1) (𝓝 1) := by
    simpa only [Gammaℝ_one, inv_one, mul_one] using! (completedHurwitzZetaEven_residue_one a).mul
      <| (differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds

Goal state after:
a : UnitAddCircle
this : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
⊢ Fermat42 a b c ↔ Fermat42 b a c

Tactic:
delta Fermat42
  rw [add_comm]
  tauto

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
⊢ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) / 2) = 1

Tactic:
Int.mul_ediv_cancel_left _ h20

Goal state after:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
⊢ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
⊢ h.IsPrimitiveClassified

Tactic:
let w := (y : ℚ) / z

Goal state after:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
h : (mk φ).embedding = φ
⊢ ComplexEmbedding.IsReal φ

Tactic:
rwa [h] at hφ

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ∀ (x : K), (Polynomial.map (algebraMap ℚ ℂ) (minpoly ℚ x)).Splits

Tactic:
exact fun x ↦ IsAlgClosed.splits _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ∀ a ∈ Finset.univ.erase w₁, f a ^ a.mult ≠ 0

Tactic:
exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
x✝ : (InfinitePlace.mk φ).embedding = φ ∨ (InfinitePlace.mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ x φ = 0

Tactic:
cases embedding_mk_eq φ with

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ IsUnramified k (mk φ)

Tactic:
isUnramified_iff,

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ (mk φ).IsReal ∨ ((mk φ).comap (algebraMap k K)).IsComplex
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ (if w.IsReal then w x else w x) = w x

Tactic:
ite_id

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

Tactic:
rw [← not_iff_not]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ¬mixedEmbedding.norm x ≠ 0 ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ volume {x | convexBodySumFun x < 1} = ↑(convexBodySumFactor K)

Tactic:
measure_lt_one_eq_integral_div_gamma (g := fun x : (mixedSpace K) => convexBodySumFun x)
      volume ((convexBodySumFun_eq_zero_iff 0).mpr rfl) convexBodySumFun_neg convexBodySumFun_add_le
      (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx)
      (fun r x => le_of_eq (convexBodySumFun_smul r x)) zero_lt_one

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal
      ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / Gamma (↑(finrank ℝ (mixedSpace K)) / 1 + 1)) =
    ↑(convexBodySumFactor K)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ ¬IsUnramified k w ↔ Nat.card ↥(Stab w) = 2

Tactic:
isUnramified_iff_card_stabilizer_eq_one

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w

Tactic:
isUnramified_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ (σ • w).IsReal ∨ ((σ • w).comap (algebraMap k K)).IsComplex ↔ IsUnramified k w
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ (σ • w).IsReal ∨ ((σ • w).comap (algebraMap k K)).IsComplex ↔ IsUnramified k w

Tactic:
isUnramified_iff,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ (σ • w).IsReal ∨ ((σ • w).comap (algebraMap k K)).IsComplex ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace k
hw : ¬IsUnramifiedIn K w
⊢ Even (Nat.card Gal(K/k))

Tactic:
by
  obtain ⟨v, rfl⟩ := comap_surjective (K := K) w
  rw [isUnramifiedIn_comap] at hw
  exact even_card_aut_of_not_isUnramified hw

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ (latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) =
    (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))

Tactic:
rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I
⊢ ((latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det =
    ((algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))).det
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2

Tactic:
· rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2

Goal state after: