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

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝ : DecidableEq L := Classical.decEq L
this : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
⊢ Fintype (ClassGroup S)

Tactic:
letI := IsIntegralClosure.isDedekindDomain R K L S

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝¹ : DecidableEq L := Classical.decEq L
this✝ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
⊢ Fintype (ClassGroup S)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ g ↑↑t = ↑(↑t ^ (χ₀ n g).val)

Tactic:
rw [modularCyclotomicCharacter.aux_spec g n t, ← zpow_natCast, modularCyclotomicCharacter.toFun,
    ZMod.val_intCast, ← Subgroup.coe_zpow]

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ↑(π ⌊x⌋₊) * log x

Tactic:
← psi_le_primeCounting_mul_log',

Goal state after:
x : ℝ
hx : 1 < x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ x
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
← psi_le_primeCounting_mul_log',

Goal state after:
x : ℝ
⊢ θ x ≤ ψ x
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
⊢ discr ℚ ⇑b = discr ℚ ⇑b'

Tactic:
← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b',

Goal state after:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
⊢ discr ℚ ⇑b =
    discr ℚ
      (Matrix.vecMul (⇑(b.reindex (b.indexEquiv b')))
        (((b.reindex (b.indexEquiv b')).toMatrix ⇑b').map ⇑(algebraMap ℚ K)))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: case e_a.inr
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
hunit : IsUnit r
hm : r = -1
⊢ (algebraMap ℤ ℚ) 1 = (algebraMap ℤ ℚ) r ^ 2

Tactic:
simp [hm]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

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

pp: case e_a.refine_4
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∀ (a b : Fin pb.dim) (ha : ¬b = a), pb.lift ((e a) pb.gen) ⋯ = e a

Tactic:
· rintro a b hba ha
    rw [ha, PowerBasis.lift_gen] at hba
    exact hba.1 rfl

Goal state after:
case e_a.refine_4
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
⊢ ∀ (a b : Fin pb.dim) (ha : ¬b = a), pb.lift ((e a) pb.gen) ⋯ = e a
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ‖↑p ^ n * ↑e + ↑(↑(x.appr n) - f (N + n))‖ < ↑p ^ (-↑n)
this : ‖↑(↑(x.appr n) - f (N + n))‖ ≤ ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)

Tactic:
Padic.norm_int_le_pow_iff_dvd,

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ‖↑p ^ n * ↑e + ↑(↑(x.appr n) - f (N + n))‖ < ↑p ^ (-↑n)
this : ↑p ^ n ∣ ↑(x.appr n) - f (N + n)
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ 0 + x✝¹ x✝ = x✝¹ x✝

Tactic:
zero_add

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

Goal state before:
pp: d a b : ℤ
⊢ ↑a ∣ ↑b ↔ a ∣ b

Tactic:
intCast_dvd

Goal state after:
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ b

Tactic:
intCast_dvd

Goal state after:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im

Tactic:
apply isCoprime_of_dvd
  · rintro ⟨hre, him⟩
    obtain rfl : b = 0 := Zsqrtd.ext hre him
    rw [zero_dvd_iff] at hdvd
    simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime
  · rintro z hz - hzdvdu hzdvdv
    apply hz
    obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩
    exact hcoprime.isUnit_of_dvd' ha hb

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
il : i ≤ n - 1
ile : i = n - 1
e : 2 * xn a1 (n - 1) = xn a1 n
a2 : a = 2
s1 : n - 1 = 0
n1 : n = 1
⊢ 2 = 2 ∧ 1 = 1 ∧ 1 - 1 = 0 ∧ 1 + 1 = 2

Tactic:
exact ⟨rfl, rfl, rfl, rfl⟩

Goal state after:
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]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
⊢ j + i = 4 * n

Tactic:
rw [this, add_tsub_cancel_of_le j4n]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]

Tactic:
xn_succ_succ a1,

Goal state after:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ xn b1 (n + 2) + xn b1 n [MOD c]
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
mem_primeFactorsList'

Goal state after:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ (p : ℕ), Prime p ∧ p ∣ m ∧ m ≠ 0 → p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(N.smoothNumbersUpTo k) ≤ 2 ^ #k.primesBelow * N.sqrt

Tactic:
convert! (Finset.card_le_card <| smoothNumbersUpTo_subset_image N k).trans <| Finset.card_image_le
  simp only [Finset.card_product, Finset.card_powerset, Finset.mem_range, zero_lt_succ,
    Finset.card_erase_of_mem, Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

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

Goal state before:
pp: case pos.left.hf'
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ 0 ≤ fun n ↦ ‖f (p ^ n)‖

Tactic:
exact fun n ↦ norm_nonneg _

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

Goal state before:
pp: case pos.left.hg'
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ 0 ≤ fun m ↦ ‖f ↑m‖

Tactic:
exact fun n ↦ norm_nonneg _

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

Goal state before:
pp: f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : max 1 ⌈Real.exp 1⌉₊ ≤ n
⊢ n ≠ 0

Tactic:
omega

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

Goal state before:
pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

pp: case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
· rw [Nat.cast_one, div_one]
    obtain ⟨_, h₁, h₂⟩ := h
    rcases le_or_gt (u : ℝ) ξ with ht | ht
    · use 0
      rw [convergent_zero, Rat.intCast_inj, eq_comm, floor_eq_iff]
      convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2) <;> norm_num
    · replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
      have hξ₁ : ⌊ξ⌋ = u - 1 := by
        rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
        exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
      rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
      · rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
        exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)
      · have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 := by
          rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
          refine ⟨(fract_lt_one ξ).le, ?_⟩
          rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
          convert! h₁ using 1
          rw [sub_eq_add_neg]
          norm_num
        use 1
        simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]

Goal state after:
case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 1 / (2 * ↑q.den ^ 2) < (↑q.den * (2 * ↑q.den - 1))⁻¹

Tactic:
rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]; ring_nf; exact hq₀

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

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ g_nat 0 a t n = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
simp only [g_nat]

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x ξ : ℝ
⊢ (fun ξ ↦ rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re) (ξ + 1) =
    (fun ξ ↦ rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re) ξ

Tactic:
simp only [ofReal_add, ofReal_one, add_mul, one_mul, jacobiTheta₂_add_left']

Goal state after:
a : UnitAddCircle
x ξ : ℝ
⊢ rexp (-π * (ξ + 1) ^ 2 * x) *
      (cexp (-↑π * I * (I * ↑x + 2 * (↑ξ * I * ↑x))) * jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re =
    rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
have (n : ℤ) : jacobiTheta₂'_term n (z + τ) τ =
      cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ -
      2 * π * I * jacobiTheta₂_term (n + 1) z τ) := by
    simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
    conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
      mul_add, mul_one, add_sub_cancel_right]
    congr 2
    ring

Goal state after:
case inr
z τ : ℂ
hτ : 0 < τ.im
this :
  ∀ (n : ℤ),
    jacobiTheta₂'_term n (z + τ) τ =
      cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 0

Tactic:
by
  induction a using QuotientAddGroup.induction_on with | H a' =>
  rw [← ofReal_eq_zero, oddKernel_def', jacobiTheta₂_undef, jacobiTheta₂'_undef, zero_div, zero_add,
    mul_zero, mul_zero] <;>
  simpa

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

Goal state before:
pp: case inr
s : ℂ
hs : s ≠ 0
⊢ (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2)) =
    (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * Gamma (s / 2 + 1))

Tactic:
Gamma_add_one (s / 2) (by grind)

Goal state after:
case inr
s : ℂ
hs : s ≠ 0
⊢ (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2)) =
    (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑π ^ (-s / 2) * (s / 2 * Gamma (s / 2)))
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ Summable fun n ↦ 1 / ↑n ^ s

Tactic:
rwa [Complex.summable_one_div_nat_cpow]

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

Goal state before:
pp: N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x ↦ χ ↑x).IsMultiplicative

Tactic:
refine IsMultiplicative.iff_ne_zero.mpr ⟨?_, fun {m} {n} hm hn _ ↦ ?_⟩

Goal state after:
case refine_1
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
⊢ (toArithmeticFunction fun x ↦ χ ↑x) 1 = 1

case refine_2
N : ℕ
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R N
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
x✝ : m.Coprime n
⊢ (toArithmeticFunction fun x ↦ χ ↑x) (m * n) =
    (toArithmeticFunction fun x ↦ χ ↑x) m * (toArithmeticFunction fun x ↦ χ ↑x) n
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
⊢ ↑((2 * N₀).smoothNumbersUpTo k).card + ↑((2 * N₀).roughNumbersUpTo k).card ≤
    ↑m * ↑(2 * N₀).sqrt + ↑((2 * N₀).roughNumbersUpTo k).card

Tactic:
by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ abscissaOfAbsConv 1 < ↑s.re

Tactic:
rw [abscissaOfAbsConv_one]; exact_mod_cast hs

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
hsum : Summable fun n ↦ ‖(riemannZetaSummandHom ⋯) n‖
⊢ 0 + ∑' (b : ℕ), (riemannZetaSummandHom ⋯) (b + 1) = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
zero_add

Goal state after:
s : ℂ
hs : 1 < s.re
hsum : Summable fun n ↦ ‖(riemannZetaSummandHom ⋯) n‖
⊢ ∑' (b : ℕ), (riemannZetaSummandHom ⋯) (b + 1) = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree

Tactic:
have hb : b ≠ 0 := by intro h; subst h; rw [wronskian_zero_right] at hw; exact hw rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).natDegree < a.natDegree + b.natDegree
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = 0 + derivative a * b
⊢ derivative a = 0 ∧ derivative b = 0

Tactic:
zero_add

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0 ∧ derivative b = 0
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (norm K) ((algebraMap (𝓞 K) (𝓞 L)) x) = x ^ finrank K L

Tactic:
RingOfIntegers.ext_iff,

Goal state after:
L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ ↑((norm K) ((algebraMap (𝓞 K) (𝓞 L)) x)) = ↑(x ^ finrank K L)
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra K F
inst✝³ : FiniteDimensional K F
inst✝² : Algebra F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : 𝓞 L
⊢ (norm K) ((norm F) x) = (norm K) x

Tactic:
RingOfIntegers.ext_iff,

Goal state after:
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
F : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Algebra K F
inst✝³ : FiniteDimensional K F
inst✝² : Algebra F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : 𝓞 L
⊢ ↑((norm K) ((norm F) x)) = ↑((norm K) x)
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : I.den • a • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : a • I.den • ↑I = a • Submodule.map (Algebra.linearMap R K) I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
smul_comm

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : a • I.den • ↑I = a • Submodule.map (Algebra.linearMap R K) I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
⊢ (↑↑ψ).toFun = ⇑K.subtype

Tactic:
have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using! hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)

Goal state after:
case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
⊢ (↑↑ψ).toFun = ⇑K.subtype