mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p q : R[X][Y]
hp : (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) p) = (aeval y) ((Transcendental.algEquivAdjoin hx) p)
hq : (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) q) = (aeval y) ((Transcendental.algEquivAdjoin hx) q)
⊢ (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) (p + q)) = (aeval y) ((Transcendental.algEquivAdjoin hx) (p + q))

Tactic:
simp_all [map_add]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
obtain ⟨N₇, h7⟩ := psi_pow_eq_sum_b x 7 hx

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ↑(∑ x ∈ range (⌊x⌋₊ + 1) with Nat.Prime x, 1) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
range_succ_eq_Icc_zero,

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ↑(∑ x ∈ Icc 0 ⌊x⌋₊ with Nat.Prime x, 1) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_1.refine_2
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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) 0 % b)) <
    cardPowDegree b • ε
⊢ False

Tactic:
rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
      have := (Classical.choose_spec (hg j₁)).2
      contradiction

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : n < p
⊢ (↑n).zmodRepr = n

Tactic:
rw [zmodRepr_natCast (p := p) n, Nat.mod_eq_of_lt hn]

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

Goal state before:
pp: case succ
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
n : ℕ
IH : ↑(p ^ k) ∣ f (k + n) - f k
this : ↑(p ^ k) ∣ ↑p ^ (k + n)
⊢ ↑(p ^ k) ∣ f (k + (n + 1)) - f k

Tactic:
simpa using! (this.trans (hi _)).add IH

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f + g)

Tactic:
rw [← sub_neg_eq_add]

Goal state after:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d a b : ℤ
⊢ ↑a ∣ ↑b ↔ a ∣ b

Tactic:
rw [intCast_dvd]

Goal state after:
d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ ↑z ∣ b

Tactic:
rw [intCast_dvd]

Goal state after:
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ b.re ∧ z ∣ b.im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b

Tactic:
try rw [inv]; rfl

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

Goal state before:
pp: case mpr
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → z.norm = 0

Tactic:
rintro rfl
    exact norm_zero

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case neg
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
· suffices a.re * a.re = 0 by
      rw [eq_zero_of_mul_self_eq_zero this] at ha ⊢
      simpa only [true_and, or_self_right, re_zero, im_zero, eq_self_iff_true, zero_eq_mul,
        mul_zero, mul_eq_zero, h.ne, false_or, or_self_iff] using ha
    apply _root_.le_antisymm _ (mul_self_nonneg _)
    rw [ha, mul_assoc]
    exact mul_nonpos_of_nonpos_of_nonneg h.le (mul_self_nonneg _)

Goal state after:
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)| ≤ 1 / (↑n + 1) / ↑(↑j / ↑k).den

Tactic:
le_div_iff₀ (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)

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)| * ↑(↑j / ↑k).den ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
x✝ : a = 2 ∧ n = 1 ∧ 0 = 0 ∧ i + 1 = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : 0 = 0
i2 : i + 1 = 2
⊢ False

Tactic:
rw [n1, i2] at ij'; exact absurd ij' (by decide)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ HasProd (F ∘ Subtype.val) (∑' (n : ℕ), f n)

Tactic:
hasProd_subtype_iff_mulIndicator,

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ HasProd ({x | Nat.Prime x}.mulIndicator F) (∑' (n : ℕ), f n)
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
N : ℕ
⊢ ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' (m : ↑N.smoothNumbers), f ↑m

Tactic:
by
  rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have H := hasSum_deriv_of_summable_norm h₀ h₁ h₂ h₃ hys

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i ↦ deriv (fun x ↦ term f x i) s) (deriv (fun w ↦ ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ g_nat k a t n

Tactic:
g_nat

Goal state after:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ (↑n + a) ^ k * rexp (-π * (↑n + a ^ 2) * t)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
rcases hp i with hai | hpi
    · simp [hai]
    simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc]
    have := Complex.GammaIntegral_convergent hs
    rw [← mul_zero (p i), ← integrableOn_Ioi_comp_mul_left_iff _ _ hpi] at this
    refine (IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1)))
      (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_mul _
    simp_rw [mul_comm (↑(rexp _) : ℂ), ← mul_assoc, neg_mul, ofReal_mul]
    rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel₀, one_mul]
    rw [Ne, cpow_eq_zero_iff, not_and_or]
    exact Or.inl (ofReal_ne_zero.mpr hpi.ne')

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

Goal state before:
pp: case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
⊢ False

Tactic:
rcases lt_trichotomy (im z) 0 with hz | hz | hz

Goal state after:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
hz : z.im < 0
⊢ False

case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
hz : z.im = 0
⊢ False

case refine_2.inr.inr.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
hz : 0 < z.im
⊢ False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
apply mul_le_of_le_one_right (mul_nonneg pi_pos.le (pow_nonneg (abs_nonneg _) _))

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

Tactic:
f_int_ofNat _ ha.1

Goal state after:
case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_nat k a t a✝ = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
by
  unfold jacobiTheta₂' jacobiTheta₂'_term jacobiTheta₂_term
  refine tsum_congr (fun n ↦ ?_)
  simp only [mul_add, Complex.exp_add, mul_one, mul_comm _ (n : ℂ), exp_int_mul_two_pi_mul_I,
    mul_one]

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

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

Tactic:
have h : -2 * (π : ℂ) ≠ (0 : ℂ) := by
    simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero,
      OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self, not_false_eq_true]
  rw [sinKernel_def]
  refine ((hasSum_jacobiTheta₂'_term a
    (by rwa [I_mul_im, ofReal_re])).div_const _).congr_fun fun n ↦ ?_
  rw [jacobiTheta₂'_term, jacobiTheta₂_term, ofReal_exp, mul_assoc (-I * n), ← Complex.exp_add,
    eq_div_iff h, ofReal_mul, ofReal_mul, ofReal_pow, ofReal_neg, ofReal_intCast,
    mul_comm _ (-2 * π : ℂ), ← mul_assoc]
  congrm ?_ * cexp (?_ + ?_)
  · simp [mul_assoc]
  · exact mul_right_comm (2 * π * I) a n
  · simp [← mul_assoc, mul_comm _ I]

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

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 0 < riemannZeta ↑x

Tactic:
rw [← LSeries_one_eq_riemannZeta hx']

Goal state after:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 0 < L 1 ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
simp [← completedHurwitzZetaOdd_one_sub]

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
n : ℕ
hn : n ≠ 0
⊢ term (fun n ↦ χ ↑n) s n = f n

Tactic:
· simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv,
        dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]

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

Goal state before:
pp: case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := ⋯
⊢ c.natAbs ∈ S

Tactic:
rw [Set.mem_ofPred_eq]

Goal state after:
case h
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, Fermat42 s.1 s.2.1 s.2.2 ∧ c.natAbs = s.2.2.natAbs
Module: Mathlib.RingTheory.Radical.Basic

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

Tactic:
intro ha

Goal state after:
case mp
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha✝ : Irreducible a
hb : b ≠ 0
ha : a ∣ radical b
⊢ a ∣ b
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
⊢ ¬a = 0 → IsUnit a

Tactic:
intro ha

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ IsUnit a
Module: Mathlib.NumberTheory.FLT.MasonStothers

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

Tactic:
right
    rw [hw] at wab wbc
    obtain ⟨ga, gb⟩ := hab.wronskian_eq_zero_iff.mp wab.symm
    obtain ⟨_, gc⟩ := hbc.wronskian_eq_zero_iff.mp wbc.symm
    exact ⟨ga, gb, gc⟩

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
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime (C v * b ^ q) (C w * c ^ r)

Tactic:
← heq,

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
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime (C v * b ^ q) (-(C u * a ^ p + C v * b ^ q))
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : FractionalIdeal (𝓞 K)⁰ K
⊢ Module.Finite ℤ ↥↑I

Tactic:
refine Module.Finite.of_surjective
    (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm.toLinearMap (LinearEquiv.surjective _)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : FractionalIdeal (𝓞 K)⁰ K
⊢ ↑I.den ≠ 0
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
have : IsGalois F L := IsGalois.tower_top_of_isGalois K F L

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x) ↔ IsUnit x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ w.IsReal ∨ ¬w.IsReal

Tactic:
exact em _

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : orderOf ⟨-1, ⋯⟩ = 2
⊢ Even (torsionOrder K)

Tactic:
rw [even_iff_two_dvd, ← this]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : orderOf ⟨-1, ⋯⟩ = 2
⊢ orderOf ⟨-1, ⋯⟩ ∣ torsionOrder K
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 + 1 * b ^ n + -1 * c ^ n = 0
hn' : 0 < n
hone : 1 = C 1
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0

Tactic:
have hneg_one : (-1 : k[X]) = C (-1) := by simp only [map_neg, map_one]

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 + -1 * c ^ n = 0
hn' : 0 < n
hone : 1 = C 1
hneg_one : -1 = C (-1)
⊢ a.natDegree = 0 ∧ b.natDegree = 0 ∧ c.natDegree = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝³ x✝² : (K →+* ℂ) → ℂ
x✝¹ : x✝³ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
x✝ : x✝² ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝³ φ) = x✝³ (ComplexEmbedding.conjugate φ)
hy : (starRingEnd ℂ) (x✝² φ) = x✝² (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((x✝³ + x✝²) φ) = (x✝³ + x✝²) (ComplexEmbedding.conjugate φ)

pp: case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)

Tactic:
· rw [Pi.add_apply, Pi.add_apply, map_add, hx, hy]

Goal state after:
case refine_4
K : Type u_1
inst✝ : Field K
x : (K →+* ℂ) → ℂ
φ : K →+* ℂ
hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
a : ℝ
x✝¹ : (K →+* ℂ) → ℂ
x✝ : x✝¹ ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)
⊢ (starRingEnd ℂ) ((a • x✝¹) φ) = (a • x✝¹) (ComplexEmbedding.conjugate φ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ ↦ ‖φ x‖₊

Tactic:
Pi.nnnorm_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (Finset.univ.sup fun b ↦ ‖(canonicalEmbedding K) x b‖₊) = Finset.univ.sup fun φ ↦ ‖φ x‖₊
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(latticeBasis K)) ↔ x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range

Tactic:
rw [show Set.range (latticeBasis K) =
      (canonicalEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
⊢ x ∈ Submodule.span ℤ (⇑(canonicalEmbedding K).toIntAlgHom.toLinearMap '' Set.range ⇑(integralBasis K)) ↔
    x ∈ ((canonicalEmbedding K).comp (algebraMap (𝓞 K) K)).range
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x = 0 ↔ x = 0

Tactic:
by
  rw [← forall_normAtPlace_eq_zero_iff, convexBodySumFun, Finset.sum_eq_zero_iff_of_nonneg
    fun _ _ ↦ mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _)]
  simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ max ‖x.1‖₊ ‖x.2‖₊ =
    max (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))
      (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))

Tactic:
Pi.nnnorm_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ max (univ.sup fun b ↦ ‖x.1 b‖₊) ‖x.2‖₊ =
    max (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))
      (univ.sup ((fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯) ∘ fun w ↦ ↑w))