mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)

Tactic:
have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd

Goal state after:
case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ ↑pb.dim * ↑pb.dim - (↑(pb.dim * (pb.dim - 1) / 2) + ↑pb.dim) = ↑(n * (n - 1) / 2)
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
a : S
i j : ι
⊢ (algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) i j =
    (leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a) i j

Tactic:
simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
    Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
y0l : 0 < { re := x - x, im := y - -y }
hn : { re := x, im := -y } ≤ { re := ↑a, im := -1 }
⊢ False

Tactic:
by
              have t := mul_le_mul_of_nonneg_right
                      (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
              rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
              exact ha t

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

Goal state before:
pp: case nonzero
d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ ¬(b.re = 0 ∧ b.im = 0)

Tactic:
rintro ⟨hre, him⟩
    obtain rfl : b = 0 := Zsqrtd.ext hre him
    rw [zero_dvd_iff] at hdvd
    simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
rcases s with a | b <;> dsimp [(· ∘ ·)]

Goal state after:
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
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ yn a1 m < yn a1 (n + 1)

Tactic:
by
    have : yn a1 m ≤ yn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl)
        fun e => by rw [e]
    simp only [yn_succ, gt_iff_lt]; refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)
    rw [← mul_one (yn a1 m)]
    exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ xn a1 m < xn a1 (n + 1)

Tactic:
have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
        fun e => by rw [e]
    simp only [xn_succ, gt_iff_lt]
    refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)
    have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
    rwa [mul_one] at t

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
have ht : b ≤ a ∨ a ≤ b := by
      have t := (a - b).nonneg_total
      rwa [neg_sub] at t
    exact (and_iff_right_of_imp ht.resolve_left).symm

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
y n : ℕ
this : 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n)
⊢ 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣
    (↑(2 * a) * yz a1 (n + 1) - yz a1 n) * (↑a - ↑y) + ↑(y ^ (n + 2)) - (↑(2 * a) * xz a1 (n + 1) - xz a1 n)

Tactic:
x_sub_y_dvd_pow_lem ↑(y ^ (n + 2)) ↑(y ^ (n + 1)) ↑(y ^ n)

Goal state after:
a : ℕ
a1 : 1 < a
y n : ℕ
this : 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n)
⊢ 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣
    ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n) +
        ↑(2 * a) * (yz a1 (n + 1) * (↑a - ↑y) + ↑(y ^ (n + 1)) - xz a1 (n + 1)) -
      (yz a1 n * (↑a - ↑y) + ↑(y ^ n) - xz a1 n)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j

Tactic:
simp [add_mul, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ ↑(4 * y) ∣ ↑(b - 1)

Tactic:
rw [Int.ofNat_sub (le_of_lt b1)]

Goal state after:
a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ ↑(4 * y) ∣ ↑b - ↑1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
⊢ ↑(4 * yn a1 i) ∣ ↑(b - 1)

Tactic:
rw [Int.ofNat_sub (le_of_lt b1)]

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
⊢ ↑(4 * yn a1 i) ∣ ↑b - ↑1
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
simp_rw [← fun x ↦ sub_add_sub_cancel (P.f x) ((P.ε * ↑(x ^ (-P.k))) • P.g₀) P.f₀]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀ + ((P.ε * ↑(x ^ (-P.k))) • P.g₀ - P.f₀)) =O[𝓝[>] 0] fun x ↦ x ^ (-P.k)
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 : ι
⊢ ‖‖a i‖ * ∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

Tactic:
norm_mul ‖a i‖,

Goal state after:
case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖‖a i‖‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
| rexp (-(π * a ^ 2) * t)

Tactic:
rw [← mul_one (rexp _)]

Goal state after:
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
| rexp (-(π * a ^ 2) * t) * 1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
by
  constructor
  · rw [← summable_jacobiTheta₂_term_iff (z := z)]
    refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_
    have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
    filter_upwards [this] with n hn
    rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]
    refine le_mul_of_one_le_left (norm_nonneg _) ?_
    simp_rw [norm_mul, norm_I, norm_real, mul_one, norm_of_nonneg pi_pos.le,
      ← ofReal_ofNat, norm_real, norm_of_nonneg two_pos.le, ← ofReal_intCast, norm_real,
      Real.norm_eq_abs, ← Int.cast_abs, ← mul_assoc _ (2 * π),
      inv_mul_cancel₀ (mul_pos two_pos pi_pos).ne', one_mul]
    rw [← Int.cast_one, Int.cast_le]
    exact Int.one_le_abs hn
  · refine fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)
    rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]
    refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n)
      (norm_nonneg _) (by positivity)
    simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]

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

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂_fderiv z τ = 0

Tactic:
by
  apply tsum_eq_zero_of_not_summable
  rw [summable_jacobiTheta₂_term_fderiv_iff]
  exact not_lt.mpr hτ

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

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (fun ξ ↦ rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re) 1

Tactic:
intro ξ

Goal state after:
a : UnitAddCircle
x ξ : ℝ
⊢ (fun ξ ↦ rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re) (ξ + 1) =
    (fun ξ ↦ rexp (-π * ξ ^ 2 * x) * (jacobiTheta₂ (↑ξ * I * ↑x) (I * ↑x)).re) ξ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (fun ξ ↦ (jacobiTheta₂ (↑ξ) (I * ↑x)).re) 1

Tactic:
intro ξ

Goal state after:
a : UnitAddCircle
x ξ : ℝ
⊢ (fun ξ ↦ (jacobiTheta₂ (↑ξ) (I * ↑x)).re) (ξ + 1) = (fun ξ ↦ (jacobiTheta₂ (↑ξ) (I * ↑x)).re) ξ
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : 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)
⊢ Summable fun i ↦ ‖a i‖ / (r i ^ 2) ^ (s / 2).re

Tactic:
convert! h_sum using 3 with i

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)
i : ι
⊢ (r i ^ 2) ^ (s / 2).re = |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
zero_cpow hs₁,

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta (-a) s + I * sinZeta (-a) s))

Tactic:
Complex.sin,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta (-a) s + I * sinZeta (-a) s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
sub_sub_cancel

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a s = completedHurwitzZetaEven a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - (1 - s)) = completedHurwitzZetaEven₀ a s

Tactic:
sub_sub_cancel

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s = completedHurwitzZetaEven₀ a s
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
⊢ ↑(ζ n✝) = 1 n✝

Tactic:
by simp [hn]

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

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

Tactic:
simpa [LSeries.abscissaOfAbsConv_one] using (by exact_mod_cast hx : (1 : EReal) < x)

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

Goal state before:
pp: case neg
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit (a ^ n)
hb : IsUnit (b ^ n)
hc : IsUnit (c ^ n)
hn : ¬n = 0
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
Int.isUnit_iff

Goal state after:
case neg
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : a ^ n = 1 ∨ a ^ n = -1
hb : b ^ n = 1 ∨ b ^ n = -1
hc : c ^ n = 1 ∨ c ^ n = -1
hn : ¬n = 0
⊢ a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
⊢ False

Tactic:
obtain ⟨A, hA⟩ : d ∣ a := gcd_dvd (by simp [s])

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b

Tactic:
apply Int.isCoprime_iff_gcd_eq_one.mpr

Goal state after:
a b c : ℤ
h : Minimal a b c
⊢ a.gcd b = 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
exfalso
    apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc
    · apply Int.natCast_dvd.1
      apply Int.dvd_of_emod_eq_zero hx
    · apply Int.natCast_dvd.1
      apply Int.dvd_of_emod_eq_zero hy

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

Goal state before:
pp: case inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
exfalso
    exact ne_zero hf.1 h1.symm

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
simp only [mul_assoc, div_right_comm _ _ (Gammaℝ _),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ (2 * m).natAbs
⊢ False

Tactic:
Int.natAbs_mul

Goal state after:
case inl
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(m.gcd n)
hp2m : p ∣ Int.natAbs 2 * m.natAbs
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
Finset.disjUnion_eq_union,

Goal state after:
case inr.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ ↑p ∣ m * m

Tactic:
(by ring : m * m = m ^ 2 - n ^ 2 + n * n)

Goal state after:
case inr
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(n.gcd m)
hpn : p ∣ n.natAbs
⊢ ↑p ∣ m ^ 2 - n ^ 2 + n * n
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) ⋯

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · rw [isRelPrime_zero_left] at hc
    simp only [zero_mul, primeFactors_zero, Finset.empty_disjUnion, primeFactors_of_isUnit hc]
  obtain rfl | hb := eq_or_ne b 0
  · rw [isRelPrime_zero_right] at hc
    simp only [mul_zero, primeFactors_zero, primeFactors_of_isUnit hc, Finset.disjUnion_empty]
  classical
  rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]

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

Goal state before:
pp: case h₂
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a

Tactic:
exact divRadical_dvd_derivative a

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ ((primeFactors a).disjUnion (primeFactors b) ⋯).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Tactic:
Finset.prod_disjUnion (disjoint_primeFactors hc)

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ (∏ x ∈ primeFactors a, id x) * ∏ x ∈ primeFactors b, id x = (primeFactors a).prod id * (primeFactors b).prod id
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
by
  rw [divRadical, ← EuclideanDomain.mul_div_assoc _ radical_dvd_self,
    mul_div_cancel_left₀ _ radical_ne_zero]

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

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical (a * b) = divRadical a * divRadical b

Tactic:
symm; apply eq_divRadical
  rw [UniqueFactorizationMonoid.radical_mul hab.isRelPrime]
  rw [mul_mul_mul_comm, radical_mul_divRadical, radical_mul_divRadical]

Goal state after: