mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [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.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
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)
⊢ pb.dim = Fintype.card (L →ₐ[K] E)

Tactic:
AlgHom.card

Goal state after:
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)
⊢ pb.dim = n
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
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
σ : L →ₐ[K] E
⊢ (Polynomial.map (algebraMap K E) (minpoly K pb.gen)).IsRoot (σ pb.gen)

pp: 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
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0

Tactic:
IsRoot.def,

Goal state after:
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
σ : L →ₐ[K] E
⊢ eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0

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
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ Function.Injective ⇑(autToPow K hμ)

Tactic:
intro f g hfg
  have : f.toAlgHom = g.toAlgHom := by
    apply (hμ.powerBasis K).algHom_ext
    rw [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_toAlgHom, powerBasis_gen,
      ← autToPow_spec K hμ g, ← autToPow_spec K hμ f, hfg]
  exact AlgEquiv.coe_toAlgHom_injective this

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
by
  have hinv : IsUnit (traceMatrix K B.basis).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
  have H :
    (traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
      (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) := by
    congr; exact traceMatrix_of_basis_mulVec _ _
  have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
  suffices ∀ i, ((traceMatrix K B.basis).det • B.basis.equivFun z) i ∈ (⊥ : Subalgebra R K) by
    rw [← B.basis.sum_repr z, Finset.smul_sum]
    refine Subalgebra.sum_mem _ fun i _ => ?_
    replace this := this i
    rw [← discr_def, Pi.smul_apply, mem_bot] at this
    obtain ⟨r, hr⟩ := this
    rw [Basis.equivFun_apply] at hr
    rw [← smul_assoc, ← hr, algebraMap_smul]
    refine Subalgebra.smul_mem _ ?_ _
    rw [B.basis_eq_pow i]
    exact Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _
  intro i
  rw [← H, ← mulVec_smul] at cramer
  replace cramer := congr_arg (mulVec (traceMatrix K B.basis)⁻¹) cramer
  rw [mulVec_mulVec, nonsing_inv_mul _ hinv, mulVec_mulVec, nonsing_inv_mul _ hinv, one_mulVec,
    one_mulVec] at cramer
  rw [← congr_fun cramer i, cramer_apply, det_apply]
  refine
    Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _
  by_cases hji : j = i
  · simp only [updateCol_apply, hji, PowerBasis.coe_basis]
    exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace (hz.mul <| hint.pow _))
  · simp only [updateCol_apply, hji, PowerBasis.coe_basis]
    exact mem_bot.2
      (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
rwa [pellZd_succ, mul_assoc, a1m, mul_one] at t

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
⊢ Dioph S'

Tactic:
← Set.ext H

Goal state after:
α : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
⊢ Dioph S
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z = 0

Tactic:
ext <;> apply eq_zero_of_mul_self_eq_zero

Goal state after:
case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re * z.re = 0

case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im * z.im = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j = n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
cases jn

Goal state after:
case refl
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
⊢ xn a1 i % xn a1 n < xn a1 (n + 1) % xn a1 n
Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q

Tactic:
by
  obtain ⟨n, hn⟩ := exists_rat_eq_convergent h
  exact ⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])

Tactic:
← hx,

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ y ∧
      (xn a1 k = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          xn a1 k * xn a1 k - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * y])
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ k ≤ yn a1 k ∧
    (xn a1 k = 1 ∧ yn a1 k = 0 ∨
      ∃ u v s t b,
        xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 k] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
rw [k0]; exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
⊢ v ∈ {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S} ↔ v ∈ {v | (v ⊗ fun i ↦ (f :: fl) i v) ∈ S}

Tactic:
by
            dsimp
            congr! 3 with x
            obtain _ | _ | _ := x <;> rfl

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

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

Tactic:
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.DiophantineApproximation.Basic

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

Tactic:
have hq₂ : (0 : ℝ) < 2 * (q.den * q.den) := mul_pos zero_lt_two (mul_pos hq₀ hq₀)

Goal state after:
case refine_3
ξ : ℝ
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)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : 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
⊢ HasSum (fun i ↦ Complex.Gamma s * a i / ↑(p i) ^ s)
    (∫ (x : ℝ) in Ioi 0, ∑' (x_1 : ι), ↑x ^ (s - 1) * (a x_1 * ↑(rexp (-p x_1 * x))) ∂volume)

Tactic:
convert!
    hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_ using
    2 with i

Goal state after:
case e'_5
ι : 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 : ι
⊢ Complex.Gamma s * a i / ↑(p i) ^ s = ∫ (a_1 : ℝ) in Ioi 0, ↑a_1 ^ (s - 1) * (a i * ↑(rexp (-p i * a_1))) ∂volume

case convert_3
ι : 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 : ι
⊢ Integrable (fun t ↦ ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

case convert_4
ι : 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
⊢ Summable fun i ↦ ∫ (a_1 : ℝ) in Ioi 0, ‖↑a_1 ^ (s - 1) * (a i * ↑(rexp (-p i * a_1)))‖ ∂volume
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
by
  split_ifs with h
  · rw [h]
    have : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_zero_sub_le ht
    refine ⟨_, pi_pos, this.trans ?_⟩
    simpa using! (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux
  · simp_rw [sub_zero]
    have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_le ha ht
    refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
    simpa only [neg_mul π (a ^ 2), mul_one] using! (isBigO_refl _ _).mul isBigO_one_aux

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

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ‖↑π‖ * 1 * ‖↑n‖ = 2 * π * ↑|n|

Tactic:
Complex.norm_of_nonneg pi_pos.le,

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * π * 1 * ‖↑n‖ = 2 * π * ↑|n|
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))
n : ℤ
⊢ (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ

Tactic:
simp [jacobiTheta₂_term_fderiv, jacobiTheta₂'_term, jacobiTheta₂_term, mul_comm]

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ∃ n, ↑n + a = 0
n : ℤ
hn : ↑n + a = 0
⊢ ↑(-n) = a

Tactic:
by simpa [neg_eq_iff_add_eq_zero]

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)

Tactic:
rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]

Goal state after:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / (↑|r i| ^ s * ↑|r i|)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ ↑(oddKernel (↑a') x) = 0

Tactic:
oddKernel_def',

Goal state after:
case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ cexp (-↑π * ↑a' ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a' * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a' * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) =
    0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ ((fun s ↦ s * Λ s) / fun s ↦ s * s.Gammaℝ) s = Λ s / s.Gammaℝ

Tactic:
Pi.div_apply,

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s✝ : ℂ
hs' : s✝ ≠ 1
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
s : ℂ
hs : s ≠ 0
⊢ s * Λ s / (s * s.Gammaℝ) = Λ s / s.Gammaℝ
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
  refine this.congr' ?_
  filter_upwards [eventually_ne_nhdsWithin one_ne_zero] with s hs
  simp [hurwitzZetaEven_def_of_ne_or_ne (Or.inr hs), mul_div_assoc]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
by
  rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun i ↦ s.Gammaℝ / ↑|↑i + a| ^ s / 2 / s.Gammaℝ) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s / s.Gammaℝ)

Tactic:
exact this.congr_fun fun n ↦ by simp only [div_right_comm _ _ (Gammaℝ _),
    div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hxy : (x, y).1 ^ 2 + (x, y).2 ^ 2 = 1
hy : (x, y).2 ≠ -1
⊢ (fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) ((fun p ↦ (↑p).1 / ((↑p).2 + 1)) ⟨(x, y), ⋯⟩) =
    ⟨(x, y), ⋯⟩

Tactic:
by
    change x ^ 2 + y ^ 2 = 1 at hxy
    have h2 : y + 1 ≠ 0 := mt eq_neg_of_add_eq_zero_left hy
    have h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1) := by
      rw [(add_neg_eq_iff_eq_add.mpr hxy.symm).symm]
      ring
    have h4 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2]
      ring
    simp only [Prod.mk_inj, Subtype.mk_eq_mk]
    constructor
    · simp [field, h3]
    · grind

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : a ∣ b
hb₀ : b ≠ 0
⊢ radical a ∣ radical b

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0
  · simp
  rw [dvd_iff_normalizedFactors_le_normalizedFactors ha₀ hb₀] at h
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors]
  exact Multiset.subset_of_le h

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime a b
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c

Tactic:
rw [← IsCoprime.pow_iff hp.bot_lt hq.bot_lt, ← isCoprime_mul_units_left hCu hCv] at hab

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime b c
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I

Tactic:
by
  rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]
  simp

Goal state after:
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✝ : IsDomain K
I : FractionalIdeal R⁰ K
⊢ absNorm I = 0 ↔ I = 0

Tactic:
by
  refine ⟨fun h ↦ zero_of_num_eq_bot zero_notMem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩
  rw [absNorm_eq, div_eq_zero_iff] at h
  refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_
  simp [Algebra.norm_eq_zero_iff]

Goal state after:
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
⊢ |(Basis.localizationLocalization ℚ ℤ⁰ K b).det (Subtype.val ∘ ⇑bI)| = absNorm I

Tactic:
by
  have := IsFractionRing.nontrivial R K
  let b₀ : Basis ι ℚ K := b.localizationLocalization ℚ ℤ⁰ K
  let bI.num : Basis ι ℤ I.num := bI.map
      ((equivNum (nonZeroDivisors.coe_ne_zero _)).restrictScalars ℤ)
  rw [absNorm_eq, ← Ideal.natAbs_det_basis_change b I.num bI.num, Nat.cast_natAbs, Int.cast_abs,
    Int.cast_abs, Basis.det_apply, Basis.det_apply]
  change _ = |algebraMap ℤ ℚ _| / _
  rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
      b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
    ext : 2
    simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
      Algebra.smul_def]
    rfl]
  rw [Basis.toMatrix_smul, Matrix.det_mul, abs_mul, ← Algebra.norm_eq_matrix_det,
    Algebra.norm_localization ℤ ℤ⁰, show (Algebra.norm ℤ (den I : R) : ℚ) =
    algebraMap ℤ ℚ (Algebra.norm ℤ (den I : R)) by rfl, mul_div_assoc, mul_div_cancel₀ _ (by
    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: