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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
have hbε : 0 < cardPowDegree b • ε := by
    rw [Algebra.smul_def, eq_intCast]
    exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
  have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
  have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
  have q_pos : 0 < Fintype.card Fq := by lia
  have q_pos' : (0 : ℝ) < Fintype.card Fq := by assumption_mod_cast
  -- If `b` is already small enough, then the remainders are equal and we are done.
  by_cases! le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊
  · obtain ⟨i₀, i₁, i_ne, mod_eq⟩ :=
      exists_eq_polynomial le_rfl b le_b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb
    refine ⟨i₀, i₁, i_ne, ?_⟩
    rwa [mod_eq, sub_self, map_zero, Int.cast_zero]
  -- Otherwise, it suffices to choose two elements whose difference is of small enough degree.
  obtain ⟨i₀, i₁, i_ne, deg_lt⟩ := exists_approx_polynomial_aux le_rfl b (fun i => A i % b) fun i =>
    EuclideanDomain.mod_lt (A i) hb
  use i₀, i₁, i_ne
  -- Again, if the remainders are equal we are done.
  by_cases h : A i₁ % b = A i₀ % b
  · rwa [h, sub_self, map_zero, Int.cast_zero]
  have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h
  -- If the remainders are not equal, we'll show their difference is of small degree.
  -- In particular, we'll show the degree is less than the following:
  suffices (natDegree (A i₁ % b - A i₀ % b) : ℝ) < b.natDegree + log ε / log (Fintype.card Fq) by
    rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']
  -- And that result follows from manipulating the result from `exists_approx_polynomial_aux`
  -- to turn the `-⌈-stuff⌉₊` into `+ stuff`.
  apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
  swap
  · convert! deg_lt
    rw [degree_eq_natDegree h']; rfl
  rw [← sub_neg_eq_add, ← neg_div, Nat.cast_sub le_b.le]
  grw [← Nat.le_ceil]

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
i : ι
j : Fin (cardM bS adm).succ
⊢ μ j * s i = b * qs j i + rs j i

Tactic:
rw [r_eq, EuclideanDomain.div_add_mod]

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

Goal state before:
pp: case e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := ⋯
this : ↑p ∣ r.num - n * ↑r.den
⊢ (fun a ↦ ↑a) (⟨↑r, h⟩ * ↑r.den) = (fun a ↦ ↑a) ↑r.num

Tactic:
simp only [coe_mul, coe_natCast]

Goal state after:
case e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
this : ↑p ∣ r.num - n * ↑r.den
⊢ ↑r * ↑r.den = ↑↑r.num
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ x.appr (n + 1) < p ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val -
      x.appr m

Tactic:
· exact ih

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val -
      x.appr m
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ (traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b)).det = P.det ^ 2 * discr A b

Tactic:
traceMatrix_of_matrix_mulVec,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ (P * traceMatrix A b * Pᵀ).det = P.det ^ 2 * discr A b
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
| ↑(p ^ (k + i))

Tactic:
rw [Nat.pow_add', Nat.cast_mul]

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
| ↑(p ^ i) * ↑(p ^ k)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
⊢ ∀ (x : ℤ_[p]), ↑p ^ (n + 1) ∣ x - ↑(x.appr (n + 1))

Tactic:
| succ n ih =>

Goal state after:
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
⊢ ∑ x, ↑(pb.dim - (1 + ↑x)) = ↑(n * (n - 1) / 2)

Tactic:
add_comm 1

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
⊢ ∑ x, ↑(pb.dim - (↑x + 1)) = ↑(n * (n - 1) / 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ ((toZModPow n).comp g) x = ((toZModPow n).comp g') x

Tactic:
rw [hg n]

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ (GenContFract.of ξ).convs (n + 1) = ↑(ξ.convergent (n + 1))

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ ↑a ≠ 1
⊢ χ.toUnitHom a ≠ 1

Tactic:
contrapose hχ
    rwa [Units.ext_iff, coe_toUnitHom] at hχ

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
⊢ j ≡ j' [MOD 4 * n]

Tactic:
by delta ModEq; rw [Nat.mod_eq_of_lt jl]

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
this : xn a1 1 < u
⊢ a < u

Tactic:
by simpa using this

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

Goal state before:
pp: case succ
n : ℕ
ih : convergent 0 n = 0
⊢ convergent 0 (n + 1) = 0

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | ⟨m, property⟩ => (m.factorization p, ⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩))
    fun x ↦
    match x with
    | (e, n) => ⟨p ^ e * ↑n, ⋯⟩

Tactic:
rintro ⟨m, hm₀, hm⟩
    rw [Subtype.mk.injEq, ← primeFactorsList_count_eq, ← prod_replicate, ← prod_append]
    conv_rhs => rw [← prod_primeFactorsList hm₀]
    have : m.primeFactorsList.filter (· = p) = m.primeFactorsList.filter (· ∉ s) :=
      filter_congr <| by grind
    refine prod_eq <| (filter_eq p).symm ▸ this ▸ perm_append_comm.trans ?_
    simp only [decide_not]
    exact filter_append_perm (· ∈ s) (primeFactorsList m)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × ↑(factoredNumbers s)
| f ↑((equivProdNatFactoredNumbers hpp hp) x)

Tactic:
equivProdNatFactoredNumbers_apply',

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
hp' : p ∉ {p ∈ s | Nat.Prime p}
x : ℕ × ↑(factoredNumbers s)
| f (p ^ x.1 * ↑x.2)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ |(fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)| = |fract ξ - ↑u' / ↑v| * (↑v / ↑u' / fract ξ)

Tactic:
rw [abs_mul, abs_of_pos H₁]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i ↦ deriv (fun x ↦ term f x i) s) (deriv (fun w ↦ ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
simp_rw [(hasDerivAt_term f _ _).deriv] at H

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i ↦ -term (logMul f) s i) (deriv (fun w ↦ ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case succ
f : ℕ → ℂ
n : ℕ
ih : abscissaOfAbsConv (logMul^[n] f) = abscissaOfAbsConv f
⊢ abscissaOfAbsConv (logMul^[n + 1] f) = abscissaOfAbsConv f

Tactic:
| succ n ih =>

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

Goal state before:
pp: case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁

Goal state after:
case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
exact tendsto_exp_atTop.comp ((tendsto_natCast_atTop_atTop.const_mul_atTop
          (mul_pos two_pos pi_pos)).atTop_mul_const hz)

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

Goal state before:
pp: case e'_6
ι : 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| ^ s = ↑(r i ^ 2) ^ (s / 2)

Tactic:
← sq_abs,

Goal state after:
case e'_6
ι : 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| ^ s = ↑(|r i| ^ 2) ^ (s / 2)
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:
← sq_abs,

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

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / (s / 2 * 2)) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Tactic:
div_mul_cancel₀ _ two_ne_zero,

Goal state after:
case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) * (1 / s) =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
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:
riemannZeta_def_of_ne_zero hs,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ completedRiemannZeta s / s.Gammaℝ = (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑π ^ (-s / 2) * Gamma (s / 2))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).k

Tactic:
change s / 2 ≠ ↑(1 / 2 : ℝ)

Goal state after:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0 ∨ a ≠ 0
hs' : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
rw [aux, div_zero, zero_div, add_zero] at hint

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
aux : ↑|0| ^ s = 0
hint :
  HasSum
    (fun n ↦
      s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedCosZeta (↑a) s)
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(Λ n)) s = -deriv (L 1) s / L 1 s

Tactic:
refine (LSeries_congr (fun {n} _ ↦ ?_) s).trans <|
    LSeries_modOne_eq ▸ LSeries_twist_vonMangoldt_eq χ₁ hs

Goal state after:
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ : n ≠ 0
⊢ ↑(Λ n) = ((fun n ↦ 1 ↑n) * fun n ↦ ↑(Λ n)) n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.refine_2
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
⊢ p ∣ 1

Tactic:
· 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: case left
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
⊢ Fermat42 a b (-c)

Tactic:
apply And.intro ha (And.intro hb _)
    rw [heq]
    exact (neg_sq c).symm

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑k * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)

Tactic:
rw [mul_comm x0, mul_comm y0, mul_iff k hk] at h

Goal state after:
case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple x0 y0 z0
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑k) (y0 * ↑k / ↑k) (↑k * z0 / ↑k)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
h2 : 1 + 1 = 2
⊢ 2 = 1 + 1 ^ 2

Tactic:
rw [one_pow 2, h2]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
⊢ divRadical (x * y) ∣ derivative (x * y)

Tactic:
have hc : IsCoprime x y :=
      EuclideanDomain.isCoprime_of_dvd
        (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy)))
        fun p hp _ hpx hpy => hp (hpxy hpx hpy)

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x y : k[X]
hpxy : IsRelPrime x y
hx : divRadical x ∣ derivative x
hy : divRadical y ∣ derivative y
hc : IsCoprime x y
⊢ divRadical (x * y) ∣ derivative (x * y)
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:
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: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ radical (a * b) = radical a * radical b

Tactic:
radical

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
have hz : z ≠ 0 := ne_of_gt hzpos

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
m n : ℤ
hm2n2 : 0 < m ^ 2 + n ^ 2
hv2 : ↑x / ↑z = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hw2 : ↑y / ↑z = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
H : (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hz : z ≠ 0
⊢ h.IsPrimitiveClassified