mathlib-initiative/mathlib-tactics huggingface dataset:
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
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf hζ.toRootsOfUnity]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x

Tactic:
← Subgroup.orderOf_coe,

Goal state after:
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
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf ↑hζ.toRootsOfUnity]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
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
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
⊢ (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun
      ((fun t ↦ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) x) =
    x

Tactic:
by
      simp only [MonoidHom.toFun_eq_coe]
      generalize_proofs _ h
      have key := hζ.autToPow_spec K ((hζ.powerBasis K).equivOfMinpoly ((hμ x).powerBasis K) h)
      have := (hζ.powerBasis K).equivOfMinpoly_gen ((hμ x).powerBasis K) h
      rw [hζ.powerBasis_gen K] at this
      rw [this, IsPrimitiveRoot.powerBasis_gen] at key
      nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key
      simp only [← rootsOfUnity.coe_pow] at key
      replace key := rootsOfUnity.coe_injective key
      rw [pow_eq_pow_iff_modEq, ← Subgroup.orderOf_coe, ← orderOf_units, hζ.val_toRootsOfUnity_coe,
        ← (zeta_spec n K L).eq_orderOf, ← ZMod.natCast_eq_natCast_iff] at key
      simp only [ZMod.natCast_val, ZMod.cast_id', id] at key
      exact Units.ext key

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = (RingHom.id ℤ_[p]) z

Tactic:
lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (RingHom.id ℤ_[p]) z = (RingHom.id ℤ_[p]) z

p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ∀ (n : ℕ), (toZModPow n).comp (RingHom.id ℤ_[p]) = toZModPow n
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inl
k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hp : Fact (Nat.Prime 2)
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : 2 ^ (k + 1) ≠ 2
hne : NeZero ↑(2 ^ (k + 1))
hp2 : 2 = 2 → k ≠ 0
⊢ (-1) ^ (2 ^ k * (2 - 1) * (2 ^ k * (2 - 1) - 1) / 2) = (-1) ^ (2 ^ k * (2 - 1) / 2)

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
      rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]; simp only [_root_.pow_succ']
      rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
      cases k
      · simp
      · simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]

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

Goal state before:
pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im

Tactic:
apply And.imp _ _ h <;> simpa only [re_smul, im_smul] using mul_left_cancel₀ ha

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

Goal state before:
pp: c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
xz : c * (x * z) ≤ d * (y * w)
⊢ SqLe (x + z) c (y + w) d

Tactic:
simp only [SqLe, mul_assoc] at xy zw

Goal state after:
c d x y z w : ℕ
xz : c * (x * z) ≤ d * (y * w)
xy : c * (x * x) ≤ d * (y * y)
zw : c * (z * z) ≤ d * (w * w)
⊢ SqLe (x + z) c (y + w) d
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
⊢ ↑(star x).norm = ↑x.norm

Tactic:
by simp [norm_eq_mul_conj, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
two_mul,

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

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

Tactic:
apply nonnegg_neg_pos.2

Goal state after:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ SqLe (d * y) 1 x d
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
two_mul,

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 (n + n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
two_mul,

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ n + n - (n + 1) = n - 1
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:
have :
          (a.re + a.im * r : R) * (b.re + b.im * r) =
            a.re * b.re + (a.re * b.im + a.im * b.re) * r + a.im * b.im * (r * r) := by
          ring

Goal state after:
R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)
⊢ ↑(a * b).re + ↑(a * b).im * ↑r = (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: n : ℕ
⊢ convergent 0 n = 0

Tactic:
by
  induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih =>
    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.LSeries.Convolution

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

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

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

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

Tactic:
have Hv : (v * (2 * v - 1) : ℝ)⁻¹ + (v : ℝ)⁻¹ = 2 / (2 * v - 1) := by
      simp [field]

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
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < ↑(max x y) + 1
hys : ↑(max x y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(max x y) + 1)
n : ℕ
x✝ : n ≠ 0
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(max x y) + 1)

Tactic:
have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi

Goal state after:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < ↑(max x y) + 1
hys : ↑(max x y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(max x y) + 1)
n : ℕ
x✝ : n ≠ 0
hs : IsOpen {s | x < s.re}
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(max x y) + 1)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
cpow_eq_zero_iff,

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

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

Tactic:
simp_rw [hns, norm_mul, one_mul, norm_I, mul_one,
      norm_real, norm_of_nonneg pi_pos.le, ← ofReal_intCast, ← ofReal_pow, norm_real,
      Real.norm_eq_abs, Int.cast_abs, abs_pow]

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ π * |↑n| ^ 2 * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * |↑n| ^ 2
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 ↦ if r i = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
⊢ HasSum (fun i ↦ s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))

Tactic:
← sq_eq_zero_iff (a := r _)

Goal state after:
ι : 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)
⊢ HasSum (fun i ↦ s.Gammaℝ * a i / ↑|r i| ^ s) (mellin F (s / 2))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ ↑(evenKernel (↑a) x) = ↑(1 / x ^ (1 / 2)) * ↑(cosKernel (↑a) (1 / x))

Tactic:
evenKernel_def,

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

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖Real.cos (2 * π * a * (↑n + 1))‖ * rexp (-π * (↑n + 1) ^ 2 * t) ≤ HurwitzKernelBounds.f_nat 0 1 t n

Tactic:
HurwitzKernelBounds.f_nat,

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖Real.cos (2 * π * a * (↑n + 1))‖ * rexp (-π * (↑n + 1) ^ 2 * t) ≤ (↑n + 1) ^ 0 * rexp (-π * (↑n + 1) ^ 2 * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]
  refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)
  exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _]

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

Goal state before:
pp: case e'_5
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (Complex.cos (2 * ↑π * ↑a * ↑n) + Complex.sin (2 * ↑π * ↑a * ↑n) * I) / ↑n ^ s =
    Complex.cos (2 * ↑π * ↑a * ↑n) / ↑n ^ s + I * (Complex.sin (2 * ↑π * ↑a * ↑n) / ↑n ^ s)

Tactic:
rw [add_div, mul_div, mul_comm _ I]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedCosZeta a s = completedCosZeta₀ a s - 1 / s - (if a = 0 then 1 else 0) / (1 - s)

Tactic:
rw [completedCosZeta, WeakFEPair.Λ, sub_div, sub_div]
  congr 1
  · rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ)]
  · simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
by
  have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm
  simp only [QuotientAddGroup.mk_zero, completedCosZeta_zero] at this
  simp only [this, Gammaℝ_def, mul_zero, zero_mul, Real.cos_zero, ofReal_one, mul_one, mul_one_div,
    ← tsum_mul_left]
  congr 1 with n
  split_ifs with h
  · simp only [h, Nat.cast_zero, zero_cpow (Complex.ne_zero_of_one_lt_re hs), div_zero]
  · rfl

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

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

Tactic:
HurwitzKernelBounds.f_nat,

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

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

Tactic:
exact Tendsto.congr (fun x ↦ by rw [← one_div, one_div_one_div]) nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z

Tactic:
refine ⟨?_, fun h => h.mul k⟩

Goal state after:
x y z k : ℤ
hk : k ≠ 0
⊢ PythagoreanTriple (k * x) (k * y) (k * z) → PythagoreanTriple x y z
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
⊢ (r ^ 2 + s ^ 2).gcd (r * s) = 1

Tactic:
exact Int.isCoprime_iff_gcd_eq_one.mp
      (Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4))

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
⊢ False

Tactic:
obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ False
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)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ‖↑↑n ^ (-s)‖ ≤ ↑n ^ (-s.re)

Tactic:
norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)

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)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ↑n ^ (-s).re ≤ ↑n ^ (-s.re)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (radical a) a

Tactic:
by
  rw [radical, ← Finset.prod_val, primeFactors_val_eq_normalizedFactors ha]
  exact prod_normalizedFactors ha'

Goal state after:
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
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
let : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
  let L := normalClosure K F (AlgebraicClosure F)
  have : FiniteDimensional F L := FiniteDimensional.right K F L
  have : IsGalois F L := IsGalois.tower_top_of_isGalois K F L
  calc
    IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) :=
      (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
    _ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
      rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
    _ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := isUnit_norm_of_isGalois K
    _ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
    _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
    _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)

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

Goal state before:
pp: case inr
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)
dr0 : derivative a = 0 ∧ derivative b = 0 ∧ derivative (c ^ r) = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
derivative_pow_eq_zero chr

Goal state after:
case inr
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)
dr0 : derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
← Subgroup.orderOf_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ orderOf ↑⟨-1, ⋯⟩ = 2
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)
⊢ Fintype.card ↥(torsion K) = 2

Tactic:
refine (Finset.card_eq_two.2 ⟨1, ⟨-1, neg_one_mem_torsion⟩,
    by simp [← Subtype.coe_ne_coe], Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)

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