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

Goal state before:
pp: case succ
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
by_cases hk : p ^ (k + 1) = 2
    · obtain rfl : p = 2 := by
        rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
      nth_rw 2 [← pow_one 2] at hk
      replace hk := Nat.pow_right_injective rfl.le hk
      rw [add_eq_right] at hk
      subst hk
      rw [pow_one] at hζ hcycl
      have : natDegree (minpoly K ζ) = 1 := by
        rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
        exact natDegree_X_sub_C (-1)
      rcases Fin.equiv_iff_eq.2 this with ⟨e⟩
      rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]
      simp only [powerBasis_dim,
        zero_add, pow_one, totient_two, reduceDiv, pow_zero, cast_ofNat, tsub_self,
        Nat.add_one_sub_one, mul_one, mul_zero]
      simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
      convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
      · congr 1
        ext i
        simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
        suffices (e.symm i : ℕ) = 0 by simp [this]
        rw [← Nat.lt_one_iff]
        convert! (e.symm i).2
        rw [this]
      · simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]
        rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; simp
    · exact discr_prime_pow_ne_two hζ hirr hk

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
rcases lt_trichotomy x y with (h | h | h)

Goal state after:
case inl
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : x < y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

case inr.inl
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : x = y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

case inr.inr
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : y < x
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
⊢ p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0

Tactic:
show (v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ t ∘ inl) ⊗ t ∘ inr from
                funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl

Goal state after:
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
⊢ p ((v ⊗ t ∘ inl) ⊗ t ∘ inr) = 0
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
h :
  ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom),
    (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}

Tactic:
by
      rw [show (x ::ₒ v) ∘ some = v from funext fun s => rfl] at h
      obtain ⟨hf, h⟩ := h; refine ⟨hf, ?_⟩; rw [PFun.fn, h]; exact hS

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

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

Tactic:
by
  let f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
  set s := {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}
  have hinj : Function.Injective f := by
    intro a b hab
    simp only [f, Prod.mk_inj] at hab
    rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
  have H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * y⌉ - 1) (⌊ξ * y⌋ + 1) ×ˢ {y} := by
    intro xy hxy
    simp only [mem_image] at hxy
    obtain ⟨q, hq₁, hq₂⟩ := hxy
    obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
    simp_rw [mem_iUnion]
    refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
    simp only [prod_singleton, mem_image, mem_Icc]
    exact ⟨q.num, hn, hq₂⟩
  refine (Finite.subset ?_ H).of_finite_image hinj.injOn
  exact Finite.biUnion (finite_Ioc _ _) fun x _ => Finite.prod (finite_Icc _ _) (finite_singleton _)

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N : ℕ
⊢ N.smoothNumbersᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
simpa only [smoothNumbers_eq_factoredNumbers]
    using factoredNumbers_compl <| Finset.filter_subset _ (Finset.range N)

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

Tactic:
simp only [toFinset_factors, Finset.mem_powerset]
    refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩
    rw [mem_primeFactors] at hp
    exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x ↦ ‖f x‖
⊢ (1 - f p)⁻¹ = ∑' (e : ℕ), f p ^ e

Tactic:
refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x ↦ ‖f x‖
⊢ Summable fun n ↦ f p ^ n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ T * ↑n ^ 2 + -(S * 2 * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im

Tactic:
mul_comm T,

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑n ^ 2 * T + -(S * 2 * ↑|n|) ≤ ↑n ^ 2 * τ.im + 2 * ↑n * z.im
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
revert h
        simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero

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

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

Tactic:
have : ((-↑·) : ℕ → ℤ).Injective := fun _ _ ↦ by simp only [neg_inj, Nat.cast_inj, imp_self]

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

Goal state before:
pp: a : ℝ
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:
have aux' : IsBigO atTop (fun t : ℝ ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) (fun _ ↦ (1 : ℝ)) := by
    simpa only [inv_pow, one_pow] using! isBigO_one_aux.pow 2

Goal state after:
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
⊢ ∃ 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)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hx : 0 < 1
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) 1 + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 -
        P.f 1 +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) 1 + {1}.indicator (fun x ↦ P.f₀ - P.f 1) 1

pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x

Tactic:
· simp [add_comm, sub_eq_add_neg]

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ F_int 1 a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
  obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1
  obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_one (sub_nonneg.mpr ha.2.le)
  refine ⟨_, lt_min hp hq, ?_⟩
  have : F_int 1 a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht
  refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;>
  apply isBigO_exp_neg_mul_of_le
  exacts [min_le_left .., min_le_right ..]

Goal state after:
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)
i : ι
⊢ (|r i| ^ 2) ^ (s / 2).re = |r i| ^ s.re

Tactic:
← rpow_natCast_mul (abs_nonneg _),

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.AbstractFuncEq

Goal state before:
pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ -P.ε • P.g₀) =ᶠ[𝓝[≠] ↑P.k] fun s ↦ (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀

Tactic:
filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ P.k)

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs : s ≠ ↑P.k
⊢ -P.ε • P.g₀ = (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ (fun x ↦ evenKernel a x - if a = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
by
  induction a using QuotientAddGroup.induction_on with | H b =>
  obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b
  refine ⟨p, hp, (EventuallyEq.isBigO ?_).trans hp'⟩
  filter_upwards [eventually_gt_atTop 0] with t h
  simp [← (hasSum_int_evenKernel b h).tsum_eq, HurwitzKernelBounds.F_int, HurwitzKernelBounds.f_int]

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

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

Tactic:
rw [oddKernel_undef _ hx, sinKernel_undef _ (one_div_nonpos.mpr hx), mul_zero]

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 / τ).im

Tactic:
rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
simp [completedHurwitzZetaEven]

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

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ riemannZeta s = (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2))

Tactic:
rw [riemannZeta_def_of_ne_zero hs, completedRiemannZeta_eq, Gammaℝ]

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ riemannZeta (1 - s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * riemannZeta s

Tactic:
rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]

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

Goal state before:
pp: n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ a✝ ^ n + b✝ ^ n ≠ c✝ ^ n

Tactic:
rw [ha, hb, hc]

Goal state after:
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
hc : c✝ = 1
⊢ 1 ^ n + 1 ^ n ≠ 1 ^ n
Module: Mathlib.NumberTheory.FLT.Basic

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

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inl.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inl.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inl.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inr.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inr.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case neg.inr.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ a ^ n + b ^ n ≠ c ^ n

Tactic:
rw [ha, hb, hc]

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

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

Tactic:
rw [ha, hb, hc]

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

Goal state before:
pp: case inr.refine_2.inl
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a
⊢ p ∣ id x

Tactic:
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.Basic

Goal state before:
pp: case inr.refine_2.inr.inl
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = b
⊢ p ∣ id x

Tactic:
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.Basic

Goal state before:
pp: case inr.refine_2.inr.inr
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = c
⊢ p ∣ id x

Tactic:
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: 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
⊢ ↑2 ∣ 2 * (m * n)

Tactic:
exact dvd_mul_right 2 (m * n)

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
have := (hasSum_int_sinZeta a hs).nat_add_neg
  simp_rw [abs_neg, Int.sign_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero,
    Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero] at this
  simp_rw [push_cast, Complex.sin]
  refine this.congr_fun fun n ↦ ?_
  rcases ne_or_eq n 0 with h | rfl
  · simp only [neg_mul, sub_mul, div_right_comm _ (2 : ℂ), Int.sign_natCast_of_ne_zero h,
      Int.cast_one, mul_one, mul_comm I, neg_neg, ← add_div, ← sub_eq_neg_add]
    congr 5 <;> ring
  · simp

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

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0

Tactic:
rw [← dvd_derivative_iff]
      apply hc.dvd_of_dvd_mul_right
      rw [← hw]; exact dvd_mul_right _ _

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 : M
n : ℕ
hn : n ≠ 0
⊢ (primeFactors (a ^ n)).prod id = (primeFactors a).prod id

Tactic:
primeFactors_pow a hn

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 : M
⊢ radical a ∣ a

Tactic:
classical
  by_cases ha : a = 0
  · rw [ha]
    apply dvd_zero
  · rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le
    rw [primeFactors, Multiset.toFinset_val]
    apply Multiset.dedup_le

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

Goal state before:
pp: p q r a b c : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
hpa : p * a < a + b + c
hqb : q * b < a + b + c
hrc : r * c < a + b + c
⊢ False

Tactic:
suffices h : p * q * r * (a + b + c) + 1 ≤ p * q * r * (a + b + c) by simp at h
  calc
    _ = (p * a) * (q * r) + (q * b) * (r * p) + (r * c) * (p * q) + 1 := by ring
    _ ≤ (a + b + c) * (q * r) + (a + b + c) * (r * p) + (a + b + c) * (p * q) := by
      rw [Nat.succ_le_iff]
      gcongr
    _ = (q * r + r * p + p * q) * (a + b + c) := by ring
    _ ≤ _ := by gcongr

Goal state after:
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
I : FractionalIdeal R⁰ K
⊢ 0 ≤ absNorm I

Tactic:
by dsimp [absNorm]; positivity

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ z ^ 2 = (m ^ 2 + n ^ 2) ^ 2

Tactic:
rw [sq, ← h.left.eq]

Goal state after:
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = (m ^ 2 + n ^ 2) ^ 2