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

Goal state before:
pp: case inr.inr.inr.inr
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:
have : Nonneg ⟨_, _⟩ :=
      nonnegg_neg_pos.2 (sqLe_add (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))
    rw [Nat.cast_add, Nat.cast_add, neg_add] at this
    rwa [add_def]

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

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

Tactic:
by
      rw [smul_val]; simpa using! nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
let t := le_antisymm xy yx

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : 1 * (x + 1) * (x + 1) = d * (y + 1) * (y + 1) := le_antisymm xy yx
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
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
⊢ xn a1 (n - 1) * 2 ≤ xn a1 (n - 1 + 1)

Tactic:
xn_succ

Goal state after:
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) * 2 ≤ xn a1 (n - 1) * a + d a1 * yn a1 (n - 1)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑↑j / ↑↑k| * |↑k| ≤ 1 / (↑n + 1)

Tactic:
Rat.cast_intCast,

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑j / ↑↑k| * |↑k| ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑j / ↑↑k| * |↑k| ≤ 1 / (↑n + 1)

Tactic:
Rat.cast_intCast,

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑j / ↑k| * |↑k| ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : n = 0
⊢ i = j

Tactic:
by simp_all

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ v ∈ {v | f v ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S}} ↔ v ∈ {v | (f v :: v) ∈ S}

Tactic:
dsimp
    -- TODO: `apply iff_of_eq` is required here, even though `congr!` works on iff below.
    apply iff_of_eq
    congr 1
    ext x; cases x <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
N : ℕ
hN : ¬Prime N
⊢ factoredNumbers (insert N s) = factoredNumbers s

Tactic:
ext m
  refine ⟨fun hm ↦ ⟨hm.1, fun p hp ↦ ?_⟩,
          fun hm ↦ ⟨hm.1, fun p hp ↦ Finset.mem_insert_of_mem <| hm.2 p hp⟩⟩
  exact Finset.mem_of_mem_insert_of_ne (hm.2 p hp)
    fun h ↦ hN <| h ▸ prime_of_mem_primeFactorsList hp

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p.Coprime n

Tactic:
hp.coprime_iff_not_dvd,

Goal state after:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ ¬p ∣ n
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ 0

Tactic:
by simpa using h

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

Goal state before:
pp: f : ℕ → ℂ
h : f =O[atTop] fun x ↦ 1
⊢ f =O[atTop] fun n ↦ ↑n ^ 0

Tactic:
by simpa using h

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s = fun n ↦ ∑' (b : ↑((fun p ↦ p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
ext n
  rcases eq_or_ne n 0 with rfl | hn
  · -- show that both sides vanish when `n = 0`; this is the hardest part of the proof!
    refine (term_zero ..).trans ?_
    -- the right-hand sum is over the union below, but in each term, one factor is always zero
    have hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0} := by
      ext
      simp
    have : ∀ p : (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {0}, term f s p.val.1 * term g s p.val.2 = 0 := by
      rintro ⟨⟨_, _⟩, hp⟩
      rcases hS ▸ hp with ⟨rfl, -⟩ | ⟨-, rfl⟩ <;> simp
    simp [this]
  -- now `n ≠ 0`
  rw [show (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n} = n.divisorsAntidiagonal by ext; simp [hn],
    Finset.tsum_subtype' n.divisorsAntidiagonal fun p ↦ term f s p.1 * term g s p.2,
    term_convolution f g s n]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
this :
  Tendsto (fun n ↦ ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' (e : ℕ), f (p ^ e)) i) atTop
    (𝓝 (∑' (n : ℕ), f n))
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable fun n ↦ ↑|n| ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
suffices Summable (fun n : ℕ ↦ (n ^ k : ℝ) * Real.exp (-π * (T * n ^ 2 - 2 * S * n))) by
    apply Summable.of_nat_of_neg <;>
    simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]

Goal state after:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ (↑(p i) ^ (s - 1))⁻¹ * ↑(p i) ^ (s - 1) * ↑t ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * t)))

Tactic:
inv_mul_cancel₀,

Goal state after:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 * ↑t ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * t)))

case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ↑(p i) ^ (s - 1) ≠ 0
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
⊢ ∫ (x : ℝ) in Ioi 0,
      ↑x ^ (s - 1) •
        ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x) =
    ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
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]

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

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
    rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
    ring

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

Tactic:
by_cases ht : t < 1 <;> [rw [add_comm] ; skip]

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioo 0 1).indicator fun x ↦ P.f x) + (Ioi 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : ¬t < 1
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ

Tactic:
rw [jacobiTheta₂', jacobiTheta₂', ← tsum_neg, ← (Equiv.neg ℤ).tsum_eq]
  congr 1 with n
  simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
  rw [Equiv.neg_apply, ← neg_mul]
  push_cast
  ring_nf

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

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂' z τ) = jacobiTheta₂' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
by
  rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]
  congr 1 with n
  simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, map_mul, ← Complex.exp_conj, map_add, map_mul,
    ← ofReal_intCast, ← ofReal_ofNat, map_pow, conj_ofReal, conj_I]
  ring_nf

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

Goal state before:
pp: a : UnitAddCircle
⊢ ContinuousOn (sinKernel a) (Ioi 0)

Tactic:
by
  induction a using QuotientAddGroup.induction_on with | H a =>
  suffices ContinuousOn (fun x ↦ (sinKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
  simp_rw [sinKernel_def]
  apply (continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)).div_const
  have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])
  fun_prop

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

Goal state before:
pp: x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioi 1
⊢ ↑x✝¹ ∈ {s | 1 < s.re}

Tactic:
by simp_all

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

Goal state before:
pp: case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, x⁻¹ = 0 → 1 = 0

Tactic:
· exact eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 ((if a = 0 then -1 else 0) * 2⁻¹)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
ite_mul,

Goal state after:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 (if a = 0 then -1 * 2⁻¹ else 0 * 2⁻¹)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
this : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ) (𝓝[≠] 1) (𝓝 1)
s : ℂ
hs : s ≠ 0
⊢ (s - 1) * completedHurwitzZetaEven a s / s.Gammaℝ = (s - 1) * hurwitzZetaEven a s

Tactic:
simp [hurwitzZetaEven_def_of_ne_or_ne (Or.inr hs), mul_div_assoc]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)

Tactic:
MulChar.one_apply <| isUnit_of_subsingleton _,

Goal state after:
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 * ↑↑x✝ ^ (-s)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 : ℤ
⊢ ∀ (b1 c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs

Tactic:
b1

Goal state after:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 : ℤ
⊢ ∀ (c1 : ℤ), Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := ⋯
S_nonempty : S.Nonempty
m : ℕ := ⋯
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ c1.natAbs ∈ S

Tactic:
use ⟨a1, ⟨b1, c1⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
rcases Int.emod_two_eq_zero_or_one x with hx | hx

Goal state after:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: 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
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b (a + b)

Tactic:
convert! IsCoprime.add_mul_left_right hab.symm 1

Goal state after:
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
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ b = b * 1
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inr
hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p
n : ℕ
h : n ≥ 3
p : ℕ
hpprime : Nat.Prime p
hdvd : p ∣ n
hpodd : Odd p
⊢ FermatLastTheoremWith ℕ p

Tactic:
· exact hprimes p hpprime hpodd

Goal state after:
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: 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
adr_dvd_w : divRadical a ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
cdr_dvd_w : divRadical c ∣ b.wronskian c
⊢ divRadical (a * b * c) ∣ w

Tactic:
rw [← wab] at adr_dvd_w bdr_dvd_w

Goal state after:
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
adr_dvd_w : divRadical a ∣ w
bdr_dvd_w : divRadical b ∣ w
cdr_dvd_w : divRadical c ∣ b.wronskian c
⊢ divRadical (a * b * c) ∣ w
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
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |(algebraMap ℤ ℚ) ((Algebra.norm ℤ) ↑I.den)| ≠ 0

Tactic:
rw [ne_eq, abs_eq_zero, IsFractionRing.to_map_eq_zero_iff, Algebra.norm_eq_zero_iff_of_basis b]
    exact nonZeroDivisors.coe_ne_zero _

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ ∃ m n,
    x = m ^ 2 - n ^ 2 ∧
      y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
rcases le_or_gt 0 m with hm | hm

Goal state after:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
⊢ ∃ m n,
    x = m ^ 2 - n ^ 2 ∧
      y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

case inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
⊢ ∃ m n,
    x = m ^ 2 - n ^ 2 ∧
      y = 2 * m * n ∧ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
x✝ :
  (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype ∨
    (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

Tactic:
cases
      Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ‖∏ σ, σ x‖

Tactic:
rw [norm_prod, ← Fintype.prod_equiv (RingHom.equivRatAlgHom K ℂ) (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
    rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
    have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
    simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _

Goal state after:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ ((coeHom K).comp (map ↑(algebraMap (𝓞 K) K))) (x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ ↑1 ≤ ↑↑|(Algebra.norm ℤ) a|

Tactic:
Rat.cast_intCast,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
⊢ ↑1 ≤ ↑|(Algebra.norm ℤ) a|
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ ca.natDegree ≤ d

Tactic:
have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
x : ↥(torsion K)
x✝ : x ∈ Finset.univ
⊢ ↑x = ↑1 ∨ x = ⟨-1, ⋯⟩

Tactic:
← Subtype.val_inj

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
this : Fintype ↥(torsion K) := Fintype.ofFinite ↥(torsion K)
x : ↥(torsion K)
x✝ : x ∈ Finset.univ
⊢ ↑x = ↑1 ∨ ↑x = ↑⟨-1, ⋯⟩