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

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, p (v ⊗ t) = 0) ∧ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p ↦ p (v ⊗ n) = 0) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ n) = 0
⊢ q (v ⊗ n) = 0

Tactic:
exact hq

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j

Tactic:
rw [yz_sub _ h, mul_sub_left_distrib, sub_add_eq_add_sub]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(d a1) * yz a1 n * (xz a1 n * yz a1 j)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
⊢ False

Tactic:
let ⟨m, n, co, (hx : x = m * g), (hy : y = n * g)⟩ := Nat.exists_coprime _ _

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
h : x * x = d * y * y
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S S' : Set (α → ℕ)
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
q : Poly (α ⊕ γ)
qe : ∀ (v : α → ℕ), v ∈ S' ↔ ∃ t, q (v ⊗ t) = 0
v : α → ℕ
x✝ : β
⊢ (some ⊗ fun x ↦ none) (inl x✝) = some x✝

Tactic:
simp only [elim_inl]

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ ↑⌊ξ⌋ + 1 / ↑((fract ξ)⁻¹.convergent n) = ↑(↑⌊ξ⌋ + ((fract ξ)⁻¹.convergent n)⁻¹)

Tactic:
one_div

Goal state after:
case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ ↑⌊ξ⌋ + (↑((fract ξ)⁻¹.convergent n))⁻¹ = ↑(↑⌊ξ⌋ + ((fract ξ)⁻¹.convergent n)⁻¹)
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card
      ↥(mulEquivToUnitHom.symm.mapSubgroup (OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H))) =
    Nat.card (Mˣ ⧸ H)

Tactic:
Subgroup.card_mapSubgroup,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card ↥(OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H)) = Nat.card (Mˣ ⧸ H)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
⊢ ↑⌊ξ⌋ ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}

Tactic:
by simp [abs_of_nonneg, Int.fract_lt_one]

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

Goal state before:
pp: v : ℤ
hv : 0 < v
⊢ 0 < 2 * ↑v - 1

Tactic:
norm_cast; lia

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

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

Tactic:
show x = x + 1 - 1 by ring

Goal state after:
f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1
Module: Mathlib.NumberTheory.LSeries.Convergence

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

Tactic:
show x = x + 1 - 1 by ring

Goal state after:
f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ (x + 1 - 1)
⊢ abscissaOfAbsConv f ≤ ↑x + 1
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: 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

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

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

Tactic:
· simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc (a _), mul_div_assoc, integral_const_mul]
    rcases hp i with hai | hpi
    · rw [hai, zero_mul, zero_mul]
    have := integral_cpow_mul_exp_neg_mul_Ioi hs hpi
    simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this
    rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]

Goal state after:
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
t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 a t‖ ≤ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))

Tactic:
refine tsum_of_norm_bounded ?_ (f_le_g_nat 0 ha ht)

Goal state after:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 0 a t) (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖P.ε‖ * (‖↑(x ^ (-P.k))‖ * ‖P.g₀‖)) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖

Tactic:
mul_comm _ ‖P.g₀‖,

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖P.ε‖ * (‖P.g₀‖ * ‖↑(x ^ (-P.k))‖)) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (t ^ (-1))) (-s) = mellin P.g (-s / -1)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
div_neg,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (t ^ (-1))) (-s) = mellin P.g (-(-s / 1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ cosKernel (-a) x = cosKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

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

Goal state before:
pp: case e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

pp: case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Tactic:
all_goals rw [arg_ofReal_of_nonneg (abs_nonneg _)]; linarith [pi_pos]

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

Goal state before:
pp: case inr
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ jacobiTheta₂' z τ = -2 * ↑π / (-I * τ) ^ (3 / 2) * jacobiTheta₂'' z (-1 / τ)

Tactic:
jacobiTheta₂'_functional_equation,

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

Goal state before:
pp: case H
b : ℝ
⊢ ∃ p, 0 < p ∧ (fun x ↦ evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
| H b =>

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

Goal state before:
pp: ⊢ riemannZeta 0 = -1 / 2

Tactic:
simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

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

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 / 2 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))

Tactic:
div_self two_ne_zero,

Goal state after:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 1 * ↑n * ((cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

Tactic:
rcases eq_or_ne n 0 with hn | hn

Goal state after:
case inl
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n = 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

case inr
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ if n = 0 then 0 else 1) s n = 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
b : ℝ
⊢ ∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
| H b =>

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

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖sinKernel (↑a) t‖ ≤ 2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n

Tactic:
← (hasSum_nat_sinKernel a ht).tsum_eq

Goal state after:
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖∑' (b : ℕ), 2 * ↑b * Real.sin (2 * π * a * ↑b) * rexp (-π * ↑b ^ 2 * t)‖ ≤
    2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (1 / -(s - 1) + 1 / (s - 1))

Tactic:
div_neg,

Goal state after:
a : UnitAddCircle
s : ℂ
| (if a = 0 then 1 else 0) / s + (-(1 / (s - 1)) + 1 / (s - 1))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
by simpa using hs 1

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Tactic:
hurwitzZetaEven_def_of_ne_or_ne (Or.inr (by simpa using hs 1))

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedHurwitzZetaEven a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedHurwitzZetaEven a s / s.Gammaℝ)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ 0 < c ^ 2

Tactic:
← h.2.2,

Goal state after:
a b c : ℤ
h : Fermat42 a b c
⊢ 0 < a ^ 4 + b ^ 4
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (b : Primes) (b_1 : ℕ), (χ ↑↑b * ↑↑b ^ (-s)) ^ (b_1 + 1) / (↑b_1 + 1) =
    ∑' (p : Primes) (k : ℕ),
      χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1)))

Tactic:
refine tsum_congr fun p ↦ tsum_congr fun k ↦ ?_

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
p : Primes
k : ℕ
⊢ (χ ↑↑p * ↑↑p ^ (-s)) ^ (k + 1) / (↑k + 1) =
    χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1)))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
⊢ False

Tactic:
apply hp.not_dvd_one
    rw [← h]
    exact Nat.dvd_gcd (Or.resolve_left hmc h2) (Or.resolve_left hnc h2)

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a.wronskian b

Tactic:
by
  rw [wronskian]
  apply dvd_sub
  · apply dvd_mul_of_dvd_left
    exact divRadical_dvd_self a
  · apply dvd_mul_of_dvd_left
    exact divRadical_dvd_derivative a

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
⊢ a ∣ b → a ∣ radical b

Tactic:
· intro ha'
    obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd hb ha ha'
    exact hc'.dvd.trans (Finset.dvd_prod_of_mem _ (by simpa [mem_primeFactors] using hc))

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (C w * c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (C w * c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (C w * c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
radical_mul_of_isUnit_left hw.isUnit_C,

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (a ^ p) * radical (b ^ q) * radical (c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))

Tactic:
let e := ((torsion K).equivMapOfInjective (Units.complexEmbedding φ)
      (Units.complexEmbedding_injective φ)).symm.toEquiv
    rw [Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : mixedSpace K
hx : x ∈ convexBodyLT' K f w₀
⊢ -x ∈ convexBodyLT' K f w₀

Tactic:
by
  simp only [Set.mem_prod, Set.mem_pi, Set.mem_univ, mem_ball, dist_zero_right, Real.norm_eq_abs,
    true_implies, Subtype.forall, Prod.fst_neg, Pi.neg_apply, norm_neg, Prod.snd_neg] at hx ⊢
  convert! hx using 3
  split_ifs <;> simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
refine iff_of_false ?_ ?_

Goal state after:
case inl.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r

case inl.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ↑(f ((integralBasis K) i)) = ↑((Basis.restrictScalars ℚ (latticeBasis K)) i)

Tactic:
LinearMap.codRestrict_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) :=
  LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap
    ⋯
i : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (canonicalEmbedding K).toRatAlgHom.toLinearMap ((integralBasis K) i) = ↑((Basis.restrictScalars ℚ (latticeBasis K)) i)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
a✝ : InfinitePlace K
⊢ a✝ ∈ univ ↔ a✝ ∈ image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ

Tactic:
simp [isReal_or_isComplex]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
this : convexBodySum K B = {0}
⊢ volume {0} = 0

Tactic:
measure_singleton

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
this : convexBodySum K B = {0}
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ x✝ : mixedSpace K
⊢ ∏ w, (normAtPlace w) (x✝¹ * x✝) ^ w.mult = (∏ w, (normAtPlace w) x✝¹ ^ w.mult) * ∏ w, (normAtPlace w) x✝ ^ w.mult

Tactic:
simp only [map_mul, mul_pow, prod_mul_distrib]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x ((indexEquiv K) (Sum.inl x_1)) +
      ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inr x_1) *
          x ((indexEquiv K) (Sum.inr x_1))

Tactic:
← univ_product_univ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inl x_1) *
          x ((indexEquiv K) (Sum.inl x_1)) +
      ∑ x_1 ∈ univ ×ˢ univ,
        fromBlocks 1 0 0
            ((blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]).submatrix ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm
              ⇑(Equiv.prodComm (Fin 2) { w // w.IsComplex }).symm)
            c (Sum.inr x_1) *
          x ((indexEquiv K) (Sum.inr x_1))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < volume (convexBodyLT K fun w ↦ if w = w₀ then B else 1)

Tactic:
rw [convexBodyLT_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLTFactor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, (if x = w₀ then B else 1) ^ x.mult) * (if w₀ = w₀ then B else 1) ^ w₀.mult)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : w.IsReal
⊢ v.IsReal

Tactic:
rw [← not_isComplex_iff_isReal] at hw ⊢

Goal state after:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝ : w.LiesOver v
hw : ¬w.IsComplex
⊢ ¬v.IsComplex