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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - ↑(toZMod x).val ∈ maximalIdeal ℤ_[p]

Tactic:
simpa using toZMod_spec _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤
    log 4 * x / log x + ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖

Tactic:
grind [le_norm_self]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ ≤ ↑p ^ (-↑n)

Tactic:
norm_le_pow_iff_mem_span_pow

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
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)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ IsUnit r

Tactic:
obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this

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)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ IsUnit r
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
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : ‖limNthHom f_compat r - ↑(nthHom f r (max n k))‖ ≤ ↑p ^ (-↑n)
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
norm_le_pow_iff_mem_span_pow

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
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case mul
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f✝ g✝ : (α → ℕ) → ℤ
a✝¹ : IsPoly f✝
a✝ : IsPoly g✝
ihf : C ⟨f✝, a✝¹⟩
ihg : C ⟨g✝, a✝⟩
⊢ C ⟨fun x ↦ f✝ x * g✝ x, ⋯⟩

Tactic:
apply H4 _ _ ihf ihg

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n * 0) ≡ xn a1 n ^ 0 [MOD yn a1 n ^ 2] ∧ yn a1 (n * 0) ≡ 0 * xn a1 n ^ (0 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
by simp [Nat.ModEq.refl]

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]
⊢ d a1 * yn a1 (n * k) * yn a1 n ≡ 0 [MOD yn a1 n ^ 2]

Tactic:
rw [modEq_zero_iff_dvd, sq]

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]
⊢ yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]

Tactic:
rw [← ke] at xm

Goal state after:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
⊢ yn a1 n ∣ t

Tactic:
by
    let ⟨k, ke⟩ := nt
    have : yn a1 n ∣ k * xn a1 n ^ (k - 1) :=
      Nat.dvd_of_mul_dvd_mul_right (strictMono_y a1 n0l) <|
        modEq_zero_iff_dvd.1 <| by
          have xm := (xy_modEq_yn a1 n k).right; rw [← ke] at xm
          exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat
    rw [ke]
    exact dvd_mul_of_dvd_right (((xy_coprime _ _).pow_left _).symm.dvd_of_dvd_mul_right this) _

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD a - 1]

Tactic:
by simp [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD a - 1]

Tactic:
by simp [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD 2]

Tactic:
by simp [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl.inl
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
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]
            have ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n := by
              rw [← two_mul, mul_comm,
                show xn a1 n = xn a1 (n - 1 + 1) by rw [tsub_add_cancel_of_le (succ_le_of_lt npos)],
                xn_succ]
              exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)
            have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos
            have il : i ≤ n - 1 := by
              apply Nat.le_of_succ_le_succ
              rw [npm]
              exact lin
            rcases lt_or_eq_of_le il with ill | ile
            · exact lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll
            · rw [ile]
              apply lt_of_le_of_ne ll
              rw [← two_mul]
              exact fun e =>
                ntriv <| by
                  let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
                  have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
                  rw [ile, a2, n1]; 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
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 j' [MOD xn a1 n]

Tactic:
← Nat.mod_add_div j (4 * n)

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
⊢ xn a1 0 ≡ xn b1 0 [MOD c] ∧ yn a1 0 ≡ yn b1 0 [MOD c]

Tactic:
by simp [Nat.ModEq.refl]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
⊢ (factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
by
  intro n hn
  simp only [Set.mem_compl_iff, mem_factoredNumbers, Set.mem_sdiff, ne_eq, not_and, not_forall,
    exists_prop, Set.mem_singleton_iff] at hn
  simp only [Set.mem_ofPred_eq]
  obtain ⟨p, hp₁, hp₂⟩ := hn.1 hn.2
  have : N ≤ p := by
    contrapose! hp₂
    exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩
  exact this.trans <| le_of_mem_primeFactorsList hp₁

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

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

Tactic:
have hv₁ : 0 < 2 * v - 1 := by linarith only [hv]

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

Goal state before:
pp: N : ℕ
⊢ N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
by
  simpa only [smoothNumbers_eq_factoredNumbers]
    using factoredNumbers_compl <| Finset.filter_subset _ (Finset.range N)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
⊢ (f ⍟ g) 0 = 0

Tactic:
simp [convolution_def]

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

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

Tactic:
· obtain hv₀' := (aux₀ (zero_lt_two.trans_le hv)).2
    have Hv : (v * (2 * v - 1) : ℝ)⁻¹ + (v : ℝ)⁻¹ = 2 / (2 * v - 1) := by
      simp [field]
    have Huv : (u / v : ℝ) = ⌊ξ⌋ + (v : ℝ)⁻¹ := by
      rw [sub_eq_iff_eq_add'.mp huv]; simp [field]
    have h' := (abs_sub_lt_iff.mp h.2.2).1
    rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h'
    rwa [lt_sub_iff_add_lt', (by ring : (v : ℝ) + -(1 / 2) = (2 * v - 1) / 2),
      lt_inv_comm₀ (div_pos hv₀' zero_lt_two) (aux₁ hv h), inv_div]

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

Goal state before:
pp: case inr.refine_2
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ (fun x ↦ rexp (-π * a ^ 2 * x) / (1 - rexp (-π * x))) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t)

Tactic:
simpa only [mul_one] using! (isBigO_refl _ _).mul isBigO_one_aux

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Tactic:
have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) *
      jacobiTheta₂_term n (a * I * t) (I * t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    grind [I_sq]

Goal state after:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ HasSum (fun x ↦ ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
unfold jacobiTheta₂ jacobiTheta₂_term

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

Goal state before:
pp: a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 ↦ ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Tactic:
have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])

Goal state after:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 ↦ ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))

Tactic:
show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-(↑π * s / 2) * I) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (L (fun n ↦ χ ↑n) s)

Tactic:
rw [← tsum_dirichletSummand χ hs]
  convert! eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
(by ring : 1 - s + 1 = 2 - s),

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) / (1 - s + 1).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s

Tactic:
(by ring : 1 - s + 1 = 2 - s),

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2✝ : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
h2 : b' ^ 2 ≤ 0
h2' : 0 ≤ b' ^ 2
⊢ False

Tactic:
exact absurd (lt_of_le_of_ne h2' (Ne.symm (pow_ne_zero _ h2b0))) (not_lt.mpr h2)

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (-(m ^ 2 - n ^ 2)).natAbs.gcd (2 * n * m).natAbs = 1

Tactic:
(by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2)

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (2 * n * m).natAbs = 1
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case neg.refine_2
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ b.natDegree + 1 ≤ (radical (a * b * c)).natDegree

pp: case neg.refine_3
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree

Tactic:
· rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption

Goal state after:
case neg.refine_3
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
abc_dr_dvd_w : divRadical (a * b * c) ∣ w
hw : ¬w = 0
⊢ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
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 : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : I.den • Submodule.map (Algebra.linearMap R K) 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:
Submonoid.smul_def,

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' : ↑I.den • Submodule.map (Algebra.linearMap R K) 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.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 : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : ↑I.den • Submodule.map (Algebra.linearMap R K) 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:
Submonoid.smul_def,

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' : ↑I.den • Submodule.map (Algebra.linearMap R K) 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.NumberTheory.PythagoreanTriples

Goal state before:
pp: 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
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2)

Tactic:
← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)

Goal state after:
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
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) ((m ^ 2 + n ^ 2) / 2 * 2)