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

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

Tactic:
by
          cases jn
          apply Int.lt_of_ofNat_lt_ofNat
          rw [lem2 (n + 1) (Nat.lt_succ_self _) j2n,
            show 2 * n - (n + 1) = n - 1 by
              rw [two_mul, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]]
          refine lt_sub_left_of_add_lt (Int.ofNat_lt_ofNat_of_lt ?_)
          rcases lt_or_eq_of_le <| Nat.le_of_succ_le_succ ij with lin | ein
          · rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]
            have ll : xn a1 (n - 1) + xn a1 (n - 1) ≤ xn a1 n := by
              rw [← two_mul, mul_comm,
                show xn a1 n = xn a1 (n - 1 + 1) by rw [tsub_add_cancel_of_le (succ_le_of_lt npos)],
                xn_succ]
              exact le_trans (Nat.mul_le_mul_left _ a1) (Nat.le_add_right _ _)
            have npm : (n - 1).succ = n := Nat.succ_pred_eq_of_pos npos
            have il : i ≤ n - 1 := by
              apply Nat.le_of_succ_le_succ
              rw [npm]
              exact lin
            rcases lt_or_eq_of_le il with ill | ile
            · exact lt_of_lt_of_le (Nat.add_lt_add_left (strictMono_x a1 ill) _) ll
            · rw [ile]
              apply lt_of_le_of_ne ll
              rw [← two_mul]
              exact fun e =>
                ntriv <| by
                  let ⟨a2, s1⟩ :=
                    @eq_of_xn_modEq_lem2 _ a1 (n - 1)
                      (by rwa [tsub_add_cancel_of_le (succ_le_of_lt npos)])
                  have n1 : n = 1 := le_antisymm (tsub_eq_zero_iff_le.mp s1) npos
                  rw [ile, a2, n1]; exact ⟨rfl, rfl, rfl, rfl⟩
          · rw [ein, Nat.mod_self, add_zero]
            exact strictMono_x _ (Nat.pred_lt npos.ne')

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

Goal state before:
pp: ξ : ℚ
⊢ {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite

Tactic:
let f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
⊢ {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
exact ⟨hm, fun p hp' ↦ hp <| mem_primeFactors_iff_mem_primeFactorsList.mpr hp'⟩

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

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

Tactic:
abs_of_pos hv₀,

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

Goal state before:
pp: n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow

Tactic:
exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

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

Goal state before:
pp: ξ : ℝ
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)
⊢ ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹

Tactic:
rw [sub_eq_iff_eq_add'.mp huv]

Goal state after:
ξ : ℝ
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)
⊢ ↑(⌊ξ⌋ * v + 1) / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℕ), f_nat 0 0 t n - 1 = F_nat 0 1 t

Tactic:
(summable_f_nat 0 0 ht).tsum_eq_zero_add,

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ f_nat 0 0 t 0 + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case inr
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ ∃ p,
    0 < p ∧
      (fun t ↦
          rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
            a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
        fun t ↦ rexp (-p * t)

Tactic:
refine ⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩

Goal state after:
case inr.refine_1
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
⊢ (fun t ↦ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2) =O[atTop] fun t ↦ rexp (-(π * a ^ 2) * t)

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hf_sum : Summable fun n : ℤ ↦ f n (z, τ) := by
    refine (summable_pow_mul_jacobiTheta₂_term_bound S hT 0).of_norm_bounded ?_
    simpa only [pow_zero, one_mul] using! norm_jacobiTheta₂_term_le hT hz.le hτ'.le

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
hf_sum : Summable fun n ↦ f n (z, τ)
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩

Goal state after:
case H
b p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
⊢ (fun x ↦ evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =ᶠ[atTop] fun t ↦
    HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / (I * ↑x⁻¹) = I * ↑x

Tactic:
ofReal_inv,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 / (I * (↑x)⁻¹) = I * ↑x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
⊢ (↑x).arg ≠ π

Tactic:
rw [arg_ofReal_of_nonneg hx.le]

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
⊢ 0 ≠ π
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = ↑(x ^ (3 / 2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
ofReal_inv,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑(x ^ (3 / 2)))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
by
  have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by
    rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
  have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg
  rw [aux, div_zero, zero_div, add_zero] at hint
  refine hint.congr_fun fun n ↦ ?_
  split_ifs with h
  · simp only [h, Nat.cast_zero, aux, div_zero, zero_div, neg_zero, zero_add]
  · simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_natCast, Complex.cos,
      show 2 * π * a * n * I = 2 * π * I * a * n by ring, neg_mul, mul_div_assoc,
      div_right_comm _ (2 : ℂ), Int.cast_natCast, Nat.abs_cast, Int.cast_neg, mul_neg, abs_neg, ←
      mul_add, ← add_div]

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ HasSum (fun n ↦ s.Gammaℝ / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s)

Tactic:
show completedHurwitzZetaEven a s = mellin (fun t ↦ ((evenKernel (↑a) t : ℂ) -
        ↑(if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) (s / 2) by
    simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
    refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
⊢ HasSum (fun n ↦ s.Gammaℝ / ↑|↑n + a| ^ s / 2)
    (mellin (fun t ↦ (↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2) (s / 2))
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
exfalso

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
h : FermatLastTheoremWith R n
a b c : R
x✝³ : a ≠ 0
x✝² : b ≠ 0
x✝¹ : c ≠ 0
x✝ : a ^ n + b ^ n = c ^ n
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2) (hurwitzZetaEven (↑a) s)

Tactic:
by
  refine (hasSum_int_hurwitzZetaEven a hs).nat_add_neg_add_one.congr_fun fun n ↦ ?_
  simp [← abs_neg (n + 1 - a), -neg_sub, neg_sub', add_div]

Goal state after:
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

Goal state after:
case inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ False
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

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

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

pp: case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ 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:
case inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

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

case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
exfalso

Goal state after:
case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

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

Tactic:
exfalso

Goal state after:
case inl.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
⊢ False
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

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

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
⊢ ↑(x.gcd y) ∣ z

Tactic:
by_cases h0 : Int.gcd x y = 0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))

Tactic:
by_cases h0 : Int.gcd x y = 0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))
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
inst✝ : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b

Tactic:
ext p

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : NormalizationMonoid M
inst✝¹ : UniqueFactorizationMonoid M
a b : M
inst✝ : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
p : M
⊢ p ∈ primeFactors (a * b) ↔ p ∈ primeFactors a ∪ primeFactors 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
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ radical a ∣ p

Tactic:
rw [radical]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ (primeFactors a).prod id ∣ p
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
n : ℕ
p i : M
ha : radical 0 ∣ p ^ n
hi : i ∈ normalizedFactors 0
⊢ False

Tactic:
simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi

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

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
this : Nontrivial M
⊢ primeFactors (radical a) = primeFactors a

Tactic:
ext p

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
this : Nontrivial M
p : M
⊢ p ∈ primeFactors (radical a) ↔ p ∈ primeFactors a
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
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 : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
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 = 0
⊢ h.IsPrimitiveClassified

Tactic:
exfalso

Goal state after:
case neg.inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
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 : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
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 = 0
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.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 : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
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 : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
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 = 1
hn2 : n % 2 = 1
⊢ h.IsPrimitiveClassified

Tactic:
exfalso

Goal state after:
case neg.inr.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 : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
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 : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
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 = 1
hn2 : n % 2 = 1
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
⊢ h.IsClassified

Tactic:
by_cases h0 : Int.gcd x y = 0

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified

case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
⊢ h.IsClassified

Tactic:
by
  by_cases h0 : Int.gcd x y = 0
  · obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
    use 0, 1, 0
    simp [hx, hy]
  apply h.isClassified_of_normalize_isPrimitiveClassified
  apply h.normalize.isPrimitiveClassified_of_coprime
  apply Int.gcd_div_gcd_div_gcd (Nat.pos_of_ne_zero h0)

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

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree < a.natDegree + b.natDegree + c.natDegree
hqb : q * b.natDegree < a.natDegree + b.natDegree + c.natDegree
hrc : r * c.natDegree < a.natDegree + b.natDegree + c.natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
exfalso

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree < a.natDegree + b.natDegree + c.natDegree
hqb : q * b.natDegree < a.natDegree + b.natDegree + c.natDegree
hrc : r * c.natDegree < a.natDegree + b.natDegree + c.natDegree
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ z = m ^ 2 + n ^ 2 ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) ∧ 0 ≤ m

Tactic:
exfalso

Goal state after:
case h.inl.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : 0 ≤ m
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_neg : z = -(m ^ 2 + n ^ 2)
⊢ False