mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Integrable (fun t ↦ ↑t ^ (s - 1) * a i * ↑(rexp (-p i * t))) (volume.restrict (Ioi 0))

Tactic:
mul_comm _ (a i),

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
⊢ Integrable (fun t ↦ a i * ↑t ^ (s - 1) * ↑(rexp (-p i * t))) (volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (fun n ↦ ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
h : Tendsto (fun x ↦ ‖((fun x ↦ jacobiTheta₂_term x z τ) ∘ fun a ↦ ↑a) x‖) atTop (𝓝 ‖0‖)
⊢ False

Tactic:
exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)

Goal state after:
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_1 : ℝ) in Ioi 0, ‖↑a_1 ^ (s - 1) * a i * ↑(rexp (-p i * a_1))‖ ∂volume‖ = Real.Gamma s.re * (‖a i‖ / p i ^ s.re)

Tactic:
mul_comm _ (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_1 : ℝ) in Ioi 0, ‖a i * ↑a_1 ^ (s - 1) * ↑(rexp (-p i * a_1))‖ ∂volume‖ = Real.Gamma s.re * (‖a i‖ / 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 : ℝ
ht : 0 < t
⊢ rexp (-π * (a ^ 2 + 1) * t) ≤ rexp (-(π * a ^ 2) * t)

Tactic:
exp_le_exp

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

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ cexp (-↑π * ↑a' ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a' * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a' * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) =
    0

Tactic:
jacobiTheta₂_undef,

Goal state after:
case H
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ cexp (-↑π * ↑a' ^ 2 * ↑x) * (jacobiTheta₂' (↑a' * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a' * 0) = 0

case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZeta a 1))

Tactic:
simp only [hurwitzZeta, add_sub_right_comm]
  refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add
    (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto

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

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

pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
jacobiTheta₂_undef,

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

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun x ↦ jacobiTheta₂ x τ) z =
    deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
funext (jacobiTheta₂_functional_equation · τ)

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun x ↦ 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * x ^ 2 / τ) * jacobiTheta₂ (x / τ) (-1 / τ)) z =
    deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z
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:
by
  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.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0
⊢ Tendsto (fun s ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))

Tactic:
simp only [this, push_cast] at h1

Goal state after:
a : UnitAddCircle
this : (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
⊢ Tendsto (fun s ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0))
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case a
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) p

Tactic:
obtain ⟨hp₁, hp₂⟩ := mem_ofPred_eq ▸ Finset.mem_sdiff.mp hp

Goal state after:
case a
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
⊢ 1 / ↑p = ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) p
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
x : ℂ
hx : x ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) x -
      1 / (x - 1) / x.Gammaℝ =
    completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ

Tactic:
Function.update_of_ne hx

Goal state after:
a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
x : ℂ
hx : x ≠ 0
⊢ completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ =
    completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
⊢ IsCoprime a b

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF
  refine isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)
  · rintro ⟨rfl, rfl⟩
    simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff]
      at HF
    simp only [HF, Finset.mem_singleton, Finset.insert_eq_of_mem, Finset.gcd_singleton, id_eq,
      normalize_zero, zero_ne_one] at Hgcd
  · rw [← Hgcd]
    refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx
    rcases hx with hx | hx | hx <;> simp only [id_eq, hx, hpa, hpb,
      dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < p ^ 2

pp: p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Tactic:
· exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)

Goal state after:
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs

Tactic:
Int.natAbs_neg c

Goal state after:
case right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs
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
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
⊢ False

Tactic:
have hrsz : r * s ≠ 0 := by grind

Goal state after:
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
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
⊢ False
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 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
⊢ False

Tactic:
obtain ⟨k, hk⟩ := Int.sq_of_gcd_eq_one htt4 hd

Goal state after:
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 : s.gcd r = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd' : ¬r * s = -d ^ 2
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
⊢ False
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 ((primeFactors a).prod id) a

Tactic:
← Finset.prod_val,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha' : a ≠ 0
⊢ Associated (primeFactors a).val.prod a
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).prod id ∣ a

Tactic:
← Finset.prod_val,

Goal state after:
case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ (primeFactors a).val.prod ∣ a
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: 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
⊢ 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:
set w := wronskian a b with wab
  have hbc : IsCoprime b c := by
    rw [add_eq_zero_iff_neg_eq] at hsum
    rw [← hsum, IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hab.symm 1
    rw [mul_one]
  have hsum' : b + c + a = 0 := by rwa [add_rotate] at hsum
  have hca : IsCoprime c a := by
    rw [add_eq_zero_iff_neg_eq] at hsum'
    rw [← hsum', IsCoprime.neg_right_iff]
    convert! IsCoprime.add_mul_left_right hbc.symm 1
    rw [mul_one]
  have wbc : w = wronskian b c := wronskian_eq_of_sum_zero hsum
  have wca : w = wronskian c a := by
    rw [add_rotate] at hsum
    simpa only [← wbc] using wronskian_eq_of_sum_zero hsum
  -- have `divRadical x` dividing `w` for `x = a, b, c`, and use coprimality
  have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by
    have adr_dvd_w := divRadical_dvd_wronskian_left a b
    have bdr_dvd_w := divRadical_dvd_wronskian_right a b
    have cdr_dvd_w := divRadical_dvd_wronskian_right b c
    rw [← wab] at adr_dvd_w bdr_dvd_w
    rw [← wbc] at cdr_dvd_w
    rw [divRadical_mul (hca.symm.mul_left hbc), divRadical_mul hab]
    exact (hca.divRadical.symm.mul_left hbc.divRadical).mul_dvd
      (hab.divRadical.mul_dvd adr_dvd_w bdr_dvd_w) cdr_dvd_w
  by_cases hw : w = 0
  · 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⟩
  · left
    -- use `abc_subcall` three times, using the symmetry in `a, b, c`
    refine ⟨?_, ?_, ?_⟩
    · rw [mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wbc <;> assumption
    · rw [← mul_rotate] at abc_dr_dvd_w ⊢
      apply abc_subcall wca <;> assumption
    · apply abc_subcall wab <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1

Tactic:
· apply Or.intro_left
      exact And.intro hm2 hn2

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ).mapMatrix (b.toMatrix (Subtype.val ∘ ⇑bI.num)) i✝ j✝ =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝

Tactic:
bI.num,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
i✝ j✝ : ι
⊢ (algebraMap ℤ ℚ).mapMatrix (b.toMatrix (Subtype.val ∘ ⇑(bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))))) i✝ j✝ =
    b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI) i✝ j✝
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 }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (convexBodyLT' K f w₀) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))

Tactic:
simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]

Goal state after:
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ∏ i, volume (if i = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑i) ^ 2} else ball 0 ↑(f ↑i)) =
    (∏ x, ENNReal.ofReal (2 * ↑(f ↑x))) *
      ((∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi) * (4 * ↑(f ↑w₀) ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal ↔ w.IsComplex ∧ ¬(w.comap (algebraMap k K)).IsComplex

Tactic:
not_isComplex_iff_isReal

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : ¬w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding

Tactic:
· rw [isRamified_iff, isComplex_iff] at h
    exact Ne.symm (h_eq ▸ h.1)

Goal state after:
case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w₁ w₂ : InfinitePlace K
h : IsRamified k w₂
h_eq : ¬w₁ = w₂
⊢ w₁.embedding ≠ conjugate w₂.embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : w.IsReal
⊢ ‖(x + y).1 ⟨w, h✝⟩‖ ≤ ‖x.1 ⟨w, h✝⟩‖ + ‖y.1 ⟨w, h✝⟩‖

Tactic:
exact norm_add_le _ _

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(x + y).2 ⟨w, ⋯⟩‖ ≤ ‖x.2 ⟨w, ⋯⟩‖ + ‖y.2 ⟨w, ⋯⟩‖

Tactic:
exact norm_add_le _ _

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (normAtPlace w) (c • 1) = |c|

Tactic:
normAtPlace_smul,

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ |c| * (normAtPlace w) 1 = |c|
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ w, ↑w.mult * (normAtPlace w) (c • x) = |c| * ∑ w, ↑w.mult * (normAtPlace w) x

Tactic:
normAtPlace_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, ↑x_1.mult * (|c| * (normAtPlace x_1) x) = |c| * ∑ w, ↑w.mult * (normAtPlace w) x