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

Goal state before:
pp: x x✝ : ℝ
| θ x✝ / (x✝ * log x✝ ^ 2)

Tactic:
rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Goal state after:
x x✝ : ℝ
| 1 / (x✝ * log x✝ ^ 2) * ∑ a ∈ Ioc 0 ⌊x✝⌋₊, if Nat.Prime a then log ↑a else 0
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₂ : ⋯.unit ^ (aux g (p ^ (k + i)) * ↑(p ^ i) - ↑(p ^ i) * aux g (p ^ k)) = 1
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
rw [(hζ.isUnit_unit NeZero.out).zpow_eq_one_iff_dvd, mul_comm, ← mul_sub] at H₂

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 ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
⊢ χ₀ n (RingEquiv.refl L) = 1

Tactic:
refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
Module: Mathlib.RingTheory.Discriminant

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

Tactic:
have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
    refine equivOfCardEq ?_
    rw [Fintype.card_fin, AlgHom.card]
    exact (PowerBasis.finrank pb).symm

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
have hnodup : ((minpoly K pb.gen).aroots E).Nodup :=
    nodup_roots (Separable.map (Algebra.IsSeparable.isSeparable K pb.gen))

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
⊢ discr K ⇑pb.basis = (-1) ^ (n * (n - 1) / 2) * (norm K) ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
n : ℕ
IH : ↑(p ^ k) ∣ f (k + n) - f k
⊢ ↑p ^ (k + n) = ↑(p ^ k) * ↑p ^ n

Tactic:
simp [pow_add]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ 0 < 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S S' : Set (α → ℕ)
d : Dioph S
H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S'
⊢ Dioph S'

Tactic:
rwa [← Set.ext H]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ 3 ≠ 0

Tactic:
decide

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a✝ : ℕ
xy : { re := -[a✝+1], im := 0 }.Nonneg
x✝ : (-{ re := -[a✝+1], im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
decide

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
n✝ : ℕ
x✝ : { re := ↑(n✝ + 1), im := 0 }.Nonneg
yx : (-{ re := ↑(n✝ + 1), im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
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
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : i = 0
j2 : j = 2
⊢ ¬2 + 1 ≤ 2 * 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case zero
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
ij : 0 ≤ j
h : xn a1 0 ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ 0 = 0 ∧ j = 2)
ij' : 0 < j
⊢ 0 < xn a1 0 % xn a1 n

Tactic:
exact x0

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : 2 < 1
x✝ : a = 2 ∧ n = 1 ∧ 0 = 0 ∧ i + 1 = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : 0 = 0
i2 : i + 1 = 2
⊢ ¬2 < 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ ¬2 ≤ 1

Tactic:
decide

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)
⊢ 0 < 4

Tactic:
decide

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

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ s.Finite

Tactic:
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]

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

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ ¬p ∣ n

Tactic:
← mem_primeFactorsList_iff_dvd hn.1 hp

Goal state after:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
⊢ VectorAllP DiophFn (f :: fl) → Dioph {v | (v ⊗ fun i ↦ (f :: fl) i v) ∈ S}

Tactic:
simp only [vectorAllP_cons, and_imp]
        exact fun df dfl =>
          have : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl)::v ∘ inr) ∈ S} :=
            ext (diophFn_comp1 (reindex_dioph _ (some ∘ inl ⊗ none :: some ∘ inr) d) <|
                reindex_diophFn inl df)
              fun v => by
                dsimp
                -- TODO: `congr! 1; ext` should be equivalent to `congr! 1 with x`
                -- but that does not work.
                congr! 1
                ext x; obtain _ | _ | _ := x <;> rfl
          have : Dioph {v | (v ⊗ f v::fun i : Fin2 n => fl i v) ∈ S} :=
            @diophFn_compn n {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S} this _ dfl
          ext this fun v => by
            dsimp
            congr! 3 with x
            obtain _ | _ | _ := x <;> rfl

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

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

Tactic:
zero_sub

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
Module: Mathlib.NumberTheory.EulerProduct.ExpLog

Goal state before:
pp: f : ℕ →*₀ ℂ
hsum : Summable fun x ↦ ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H :
  ∏' (b : Subtype Nat.Prime), (cexp ∘ (fun b ↦ -log (1 - f b)) ∘ Subtype.val) b =
    cexp (∑' (b : Subtype Nat.Prime), ((fun b ↦ -log (1 - f b)) ∘ Subtype.val) b)
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n

Tactic:
simp only [Function.comp_apply, exp_neg, exp_log (hp _)] at H

Goal state after:
f : ℕ →*₀ ℂ
hsum : Summable fun x ↦ ‖f x‖
hs : ∀ {p : ℕ}, 1 < p → ‖f p‖ < 1
hp : ∀ (p : Nat.Primes), 1 - f ↑p ≠ 0
H : ∏' (b : Subtype Nat.Prime), (1 - f ↑b)⁻¹ = cexp (∑' (b : Subtype Nat.Prime), -log (1 - f ↑b))
⊢ cexp (∑' (p : Nat.Primes), -log (1 - f ↑p)) = ∑' (n : ℕ), f n
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})
a : EReal
⊢ ↑x < a → y ≤ a

Tactic:
replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy

Goal state after:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < a → y ≤ a
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
decide

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
⊢ f ⍟ g = fun n ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
by
  ext n
  simpa [convolution, toArithmeticFunction] using
    Finset.sum_congr rfl fun p hp ↦ by simp [ne_zero_of_mem_divisorsAntidiagonal hp]

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

Goal state before:
pp: case h.inl
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : v < 1
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

pp: case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
· replace h := h.2.2
    simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul,
      cast_zero, inv_zero] at h
    exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)

Goal state after:
case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
⊢ ∃ n, ↑u / ↑v = ξ.convergent 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 : ℤ
⊢ |↑n| * |z.im| ≤ |↑n| * S

Tactic:
exact mul_le_mul_of_nonneg_left hz (abs_nonneg _)

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

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |(↑i + a) ^ k| * |rexp (-π * (↑i + a) ^ 2 * t)| ≤ 2 ^ k * ↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t)

Tactic:
abs_exp,

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)
⊢ ∀ᶠ (i : ℕ) in atTop, |(↑i + a) ^ k| * rexp (-π * (↑i + a) ^ 2 * t) ≤ 2 ^ k * ↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
refine Iff.symm ⟨fun hτ ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
z τ : ℂ
hτ : 0 < τ.im
⊢ Summable fun x ↦ jacobiTheta₂_term x z τ

case refine_2
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
⊢ 0 < τ.im
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
zero_sub

Goal state after:
case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))
⊢ False
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
indicator_of_notMem (notMem_Ioi.mpr this.le),

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ 0 + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
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_rw [indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem (notMem_Ioo_of_ge hx'.le),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne')]

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
⊢ P.f x - P.f₀ + 0 - P.f x + P.f₀ = 0 + 0
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ ∫ (x : ℝ) in Ioi 0,
      ↑x ^ (s - 1) •
        ((Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x) =
    ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • (Ioo 0 1).indicator (fun t ↦ P.f₀ - (P.ε * ↑(t ^ (-P.k))) • P.g₀) x

Tactic:
refine setIntegral_congr_ae measurableSet_Ioi (eventually_of_mem (U := {1}ᶜ)
        (compl_mem_ae_iff.mpr (subsingleton_singleton.measure_zero _)) (fun x hx _ ↦ ?_))
    rw [indicator_of_notMem hx, add_zero]

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (x y : ℂ × ℂ →L[ℂ] ℂ), (x + y) (1, 0) = x (1, 0) + y (1, 0)

Tactic:
by simp only [add_apply, forall_const]

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

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ

Tactic:
by
  refine tsum_congr (fun n ↦ ?_)
  simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, Complex.exp_add]
  suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]
  rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
    exp_two_pi_mul_I, one_zpow]

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

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

Tactic:
by
  simp only [hurwitzZeta, add_sub_right_comm]
  exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

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

Goal state before:
pp: case inl
⊢ riemannZeta 0 = (0 * completedRiemannZeta₀ 0 - 1 - 0 / (1 - 0)) / (2 * ↑π ^ (-0 / 2) * Gamma (0 / 2 + 1))

Tactic:
simp [riemannZeta_zero]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : ∑' (n : ℕ), term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ L (fun n ↦ ↑(ζ n)) s = riemannZeta s

Tactic:
by
    simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]

Goal state after:
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
⊢ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) =ᶠ[𝓝 1] fun s ↦
    completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ

Tactic:
filter_upwards [eventually_ne_nhds one_ne_zero] with x 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
⊢ hurwitzZetaEven a x - 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 : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
rw [← Rat.num_ne_zero] at ha hb hc

Goal state after:
n : ℕ
tfae_1_to_2 : FermatLastTheoremWith ℕ n → FermatLastTheoremWith ℤ n
h : FermatLastTheoremWith ℤ n
a b c : ℚ
ha : a.num ≠ 0
hb : b.num ≠ 0
hc : c.num ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False
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
⊢ 1 + 1 ≠ 1

Tactic:
decide

Goal state after:
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
⊢ 1 + 1 ≠ -1

Tactic:
decide

Goal state after:
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
⊢ 1 + -1 ≠ 1

Tactic:
decide

Goal state after:
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
⊢ 1 + -1 ≠ -1

Tactic:
decide

Goal state after:
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
⊢ -1 + 1 ≠ 1

Tactic:
decide

Goal state after:
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
⊢ -1 + 1 ≠ -1

Tactic:
decide

Goal state after:
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
⊢ -1 + -1 ≠ 1

Tactic:
decide

Goal state after:
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
⊢ -1 + -1 ≠ -1

Tactic:
decide

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s

Tactic:
have : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (Gammaℝ (1 - s))⁻¹ := by
    rw [cosZeta, Function.update_of_ne, div_eq_mul_inv]
    simpa [sub_eq_zero] using (hs 0).symm

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case «0»
⊢ (fun i ↦ i) ⟨0, ⋯⟩ * (fun i ↦ i) ⟨0, ⋯⟩ ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case «1»
⊢ (fun i ↦ i) ⟨1, ⋯⟩ * (fun i ↦ i) ⟨1, ⋯⟩ ≠ 2

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case «2»
⊢ (fun i ↦ i) ⟨2, ⋯⟩ * (fun i ↦ i) ⟨2, ⋯⟩ ≠ 2

Tactic:
decide

Goal state after: