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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
exists_nonempty_j :
  ¬∃ j, (∃ i, t' i = j) ∧ ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i : Fin n
hi : ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
this : False
⊢ t' i = j

Tactic:
contradiction

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2 * √x) =o[atTop] fun x ↦ x

Tactic:
conv => arg 2; ext; rw [mul_comm]

Goal state after:
⊢ (fun x ↦ √x * log x ^ 2) =o[atTop] fun x ↦ x
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‖
⊢ ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
primeCounting_eq_theta_div_log_add_integral hx,

Goal state after:
ε : ℝ
ε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‖
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ (log 4 + ε) * x / log x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
intro a
    apply subset_closure
    exact Set.mem_range_self _

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a
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
⊢ ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen) =
    (algebraMap K E) ((norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen))))

Tactic:
rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]

Goal state after:
case e_a
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
⊢ ∏ i, ∏ j ∈ {i}ᶜ, ((e j) pb.gen - (e i) pb.gen) = ∏ σ, σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case pos
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
hinv : IsUnit (traceMatrix K ⇑B.basis).det
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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : j = i
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥

pp: case neg
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
hinv : IsUnit (traceMatrix K ⇑B.basis).det
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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥

Tactic:
· simp only [updateCol_apply, hji, PowerBasis.coe_basis]
    exact mem_bot.2 (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace (hz.mul <| hint.pow _))

Goal state after:
case neg
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
hinv : IsUnit (traceMatrix K ⇑B.basis).det
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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - d a1 * y * y = 1
hp : 0 = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }

Tactic:
contradiction

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

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

Tactic:
by
    simp only [muld_val]
    apply nonnegg_pos_neg.2
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
t : x + 1 = 0
⊢ False

Tactic:
contradiction

Goal state after:
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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 (2 * n - (2 * n - k)) + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
rw [tsub_tsub_cancel_of_le k2n] at t

Goal state after:
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)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
d : ℤ
f g : ℤ√d →+* R
h : f sqrtd = g sqrtd
⊢ f = g

Tactic:
by
  ext ⟨re_x, im_x⟩
  simp [decompose, h]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ ↑(a + b).re + ↑(a + b).im * ↑r = ↑a.re + ↑a.im * ↑r + (↑b.re + ↑b.im * ↑r)

Tactic:
simp only [re_add, Int.cast_add, im_add]

Goal state after:
R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ ↑a.re + ↑b.re + (↑a.im + ↑b.im) * ↑r = ↑a.re + ↑a.im * ↑r + (↑b.re + ↑b.im * ↑r)
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
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n

Tactic:
have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos

Goal state after:
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
ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n
npm : (n - 1).succ = n
⊢ xn a1 (n - 1) + xn a1 i < 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:
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h
  exact ⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩

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

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case succ
f : ℕ → ℂ
m : ℕ
ih : ∀ {s : ℂ}, abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
⊢ iteratedDeriv (m + 1) (LSeries f) s = (-1) ^ (m + 1) * LSeries (logMul^[m + 1] f) s

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

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

Goal state before:
pp: case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * ↑|n| ≤ 2 * π * ↑(|n| ^ 2)

Tactic:
← Int.le_self_sq

Goal state after:
case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * ↑|n| ≤ 2 * π * ↑|n|
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖F_nat 1 a t‖ ≤
    rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)
  unfold g_nat
  simp_rw [pow_one, add_mul]
  apply HasSum.add
  · have h0' : ‖rexp (-π * t)‖ < 1 := by
      simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht
    convert! (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1
    · ext1 n
      rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
      ring_nf
    · rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
  · convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
    ext1 n
    rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]
    ring_nf

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

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b ↦ jacobiTheta₂'_term b z τ

Tactic:
summable_jacobiTheta₂'_term_iff

Goal state after:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ 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
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))

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t)

Tactic:
rw [← hasSum_ofReal, evenKernel_def]
  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]
  simpa [this] using (hasSum_jacobiTheta₂_term _ (by simpa)).mul_left _

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

Goal state before:
pp: z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * ↑π = I * (2 * ↑π * I)

Tactic:
mul_comm I,

Goal state after:
z τ : ℂ
hτ : τ ≠ 0
⊢ -2 * ↑π = 2 * ↑π * I * I
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
jacobiTheta₂'_undef z hτ,

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

Goal state before:
pp: ⊢ (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0

Tactic:
unfold hurwitzEvenFEPair WeakFEPair.symm
  congr 1 <;> simp [evenKernel_eq_cosKernel_of_zero]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
n : ℕ
⊢ s ≠ -↑n

Tactic:
convert! hs (n + 1) using 1

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
n : ℕ
⊢ -↑n = 1 - ↑(n + 1)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

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

Tactic:
completedRiemannZeta_eq,

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

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

pp: 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

Tactic:
· simp [toArithmeticFunction]

Goal state after:
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.FLT.Basic

Goal state before:
pp: case inr.inr.inr.inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha✝ : a ≠ 0
hb✝ : b ≠ 0
hc✝ : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ False

Tactic:
refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, *]

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

Goal state before:
pp: case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp

Goal state after:
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ k ^ 4 * (a ^ 4 + b ^ 4) = k ^ 4 * c ^ 2
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ ¬IsUnit ↑p

Tactic:
ZMod.isUnit_prime_iff_not_dvd h,

Goal state after:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
⊢ ¬¬p ∣ N
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < z * z

Tactic:
rw [← h.eq, ← sq, ← sq]

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case right
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
⊢ b ∣ a * derivative b

Tactic:
rw [hw]

Goal state after:
case right
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
⊢ b ∣ derivative a * b
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ∣ normalize p

Tactic:
dvd_normalize_iff

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ∣ p
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: case hpr
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p✝ : k[X]
i✝ : ℕ
a✝ : Prime p✝
⊢ divRadical (p✝ ^ i✝) ∣ derivative (p✝ ^ i✝)

pp: case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)

Tactic:
· case hpr p i hp =>
    cases i
    · rw [pow_zero, derivative_one]
      apply dvd_zero
    · case succ i =>
      rw [← mul_dvd_mul_iff_left radical_ne_zero, radical_mul_divRadical,
        radical_pow_of_prime hp i.succ_ne_zero, derivative_pow_succ, ← mul_assoc]
      apply dvd_mul_of_dvd_left
      rw [mul_comm, mul_assoc]
      apply dvd_mul_of_dvd_right
      rw [pow_succ, mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero), dvd_normalize_iff]

Goal state after:
case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (normalizedFactors a).dedup ≤ normalizedFactors a

Tactic:
apply Multiset.dedup_le

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n, hn, by ext; rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]⟩

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)
⊢ 1 ≠ ⟨-1, ⋯⟩

Tactic:
simp [← Subtype.coe_ne_coe]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
⊢ -x ∈ convexBodyLT K f

Tactic:
simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
    mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
    Prod.snd_neg] at hx ⊢
  exact hx

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + b ^ n - c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
← one_mul (b ^ n),

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
heq : 1 * a ^ n + 1 * b ^ n - c ^ n = 0
hn' : 0 < n
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
a' : k[X]
eq_a : a = gcd a b * a'
b' : k[X]
eq_b : b = gcd a b * b'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
set d := gcd a b

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
heq : a ^ n + b ^ n = c ^ n
a' b' : k[X]
d : k[X] := gcd a b
eq_a : a = d * a'
eq_b : b = d * b'
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
⊢ (↑(integerLattice K) ∩ Metric.closedBall 0 r).Finite

Tactic:
convert! (Embeddings.finite_of_norm_le K ℂ r).image (canonicalEmbedding K)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
⊢ ↑(integerLattice K) ∩ Metric.closedBall 0 r =
    ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r}
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Function.Surjective (Quotient.lift (fun x ↦ x.comap (algebraMap k K)) ⋯)

Tactic:
intro w
    obtain ⟨w', hw⟩ := comap_surjective (K := K) w
    exact ⟨⟦w'⟧, hw⟩

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

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k φ

Tactic:
· rw [← star_star φ]; simpa [← congrArg conjugate hr] using h.isMixed_conjugate_embedding

Goal state after: