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

Goal state before:
pp: case f
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
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : L →ₐ[K] E
| eval (σ pb.gen) (Polynomial.map (algebraMap K E) (derivative (minpoly K pb.gen)))

Tactic:
← derivative_map,

Goal state after:
case f
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
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : L →ₐ[K] E
| eval (σ pb.gen) (derivative (Polynomial.map (algebraMap K E) (minpoly K pb.gen)))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det * (algebraMap ℤ ℚ) r' = 1

Tactic:
hr',

Goal state after:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det * (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det = 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist ((lift f_compat) r) (g r) ≤ ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist ((lift f_compat) r) (g r) ≤ ε
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
have H := congr_arg (@derivative K _) (cyclotomic_prime_pow_mul_X_pow_sub_one K p k)

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H : derivative (cyclotomic (p ^ (k + 1)) K * (X ^ p ^ k - 1)) = derivative (X ^ p ^ (k + 1) - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ CommRing (ℤ√d)

Tactic:
refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ }

Goal state after:
case refine_1
d : ℤ
⊢ ∀ (a b : ℤ√d), a + b = b + a

case refine_2
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * b * c = a * (b * c)

case refine_3
d : ℤ
⊢ ∀ (a : ℤ√d), 1 * a = a

case refine_4
d : ℤ
⊢ ∀ (a : ℤ√d), a * 1 = a

case refine_5
d : ℤ
⊢ ∀ (a : ℤ√d), 0 * a = 0

case refine_6
d : ℤ
⊢ ∀ (a : ℤ√d), a * 0 = 0

case refine_7
d : ℤ
⊢ ∀ (a b c : ℤ√d), a * (b + c) = a * b + a * c

case refine_8
d : ℤ
⊢ ∀ (a b c : ℤ√d), (a + b) * c = a * c + b * c

case refine_9
d : ℤ
⊢ ∀ (a b : ℤ√d), a * b = b * a
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case pos
ξ : ℝ
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
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - (↑⌊ξ * ↑m⌋ + ↑1)) * (↑n + 1)| ≤ 1

Tactic:
← sub_sub,

Goal state after:
case pos
ξ : ℝ
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
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - ↑⌊ξ * ↑m⌋ - ↑1) * (↑n + 1)| ≤ 1
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 : 2 * ↑v - 1 < 1
⊢ False

Tactic:
norm_cast at H

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 : 2 * v - 1 < 1
⊢ False
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k m : ℕ
⊢ (∃ x, m < N + 1 ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔
    ∃ a, ((a < N + 1 ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N + 1 ∧ m ≠ 0 ∧ a ∣ m

Tactic:
refine exists_congr fun p ↦ ?_

Goal state after:
N k m p : ℕ
⊢ m < N + 1 ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔
    ((p < N + 1 ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N + 1 ∧ m ≠ 0 ∧ p ∣ m
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))⁻¹
⊢ |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹

Tactic:
← sub_sub,

Goal state after:
ξ : ℝ
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))⁻¹
⊢ |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ⊆ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (x : ↑(factoredNumbers s)), f ↑x + ∑' (x : ↑(factoredNumbers s)ᶜ), f ↑x - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε

Tactic:
add_sub_cancel_left,

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ⊆ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (x : ↑(factoredNumbers s)ᶜ), f ↑x‖ < ε
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' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - (↑u' / ↑v + ↑⌊ξ⌋)
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
← sub_sub,

Goal state after:
ξ : ℝ
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' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u' / ↑v - ↑⌊ξ⌋
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_2
ξ : ℝ
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)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : ξ - (↑⌊ξ⌋ + (↑v)⁻¹) < (↑v * (2 * ↑v - 1))⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v

Tactic:
← sub_sub,

Goal state after:
case refine_2
ξ : ℝ
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)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : ξ - ↑⌊ξ⌋ - (↑v)⁻¹ < (↑v * (2 * ↑v - 1))⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ f n / ↑n ^ z) (-(logMul f n / ↑n ^ s)) s

Tactic:
← neg_div,

Goal state after:
case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ f n / ↑n ^ z) (-logMul f n / ↑n ^ s) s
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x

Tactic:
LSeries_iteratedDeriv _ h,

Goal state after:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ (-1) ^ n * ((-1) ^ n * LSeries (logMul^[n] a) ↑x)
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case succ
f : ℕ → ℂ
m : ℕ
ih : ∀ {s : ℂ}, abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
ih' : Set.EqOn (iteratedDeriv m (LSeries f)) ((-1) ^ m * LSeries (logMul^[m] f)) {s | abscissaOfAbsConv f < ↑s.re}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv ((-1) ^ m * LSeries (logMul^[m] f)) s
⊢ iteratedDeriv (m + 1) (LSeries f) s = (-1) ^ (m + 1) * LSeries (logMul^[m + 1] f) s

Tactic:
rw [iteratedDeriv_succ, this]

Goal state after:
case succ
f : ℕ → ℂ
m : ℕ
ih : ∀ {s : ℂ}, abscissaOfAbsConv f < ↑s.re → iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
ih' : Set.EqOn (iteratedDeriv m (LSeries f)) ((-1) ^ m * LSeries (logMul^[m] f)) {s | abscissaOfAbsConv f < ↑s.re}
this : deriv (iteratedDeriv m (LSeries f)) s = deriv ((-1) ^ m * LSeries (logMul^[m] f)) s
⊢ deriv ((-1) ^ m * LSeries (logMul^[m] f)) s = (-1) ^ (m + 1) * LSeries (logMul^[m + 1] f) s
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case e'_3
ξ : ℝ
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ξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) = ↑u + -(1 / 2)

Tactic:
sub_eq_add_neg

Goal state after:
case e'_3
ξ : ℝ
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ξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u + -(1 - 2⁻¹) = ↑u + -(1 / 2)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
convert! hC' using 1

Goal state after:
case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ = ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖

case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
| fun t ↦ rexp (-(π * a ^ 2) * t)

Tactic:
enter [t]

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

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ ↑(Int.negSucc n) + a = -(↑n + (1 - a))

Tactic:
by { push_cast; ring }

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

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ -↑(m + 1) + a = -(↑m + (1 - a))

Tactic:
by { push_cast; ring }

Goal state after:
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 Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀

Tactic:
← intervalIntegral.integral_of_le zero_le_one

Goal state after:
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 0..1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) • P.g₀ =
    (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5
ι : 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 : ι
⊢ s.Gammaℝ * a i = ↑π ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i

Tactic:
← neg_div,

Goal state after:
case e'_5
ι : 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 : ι
⊢ s.Gammaℝ * a i = ↑π ^ (-s / 2) * Complex.Gamma (s / 2) * a i
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    2 * ↑π * I * ↑n * cexp ((2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z))

Tactic:
congr 2

Goal state after:
case e_a
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ =
    (2 * ↑π * I * ↑n + 2 * ↑π * I) * z + ↑π * I * (↑n + 1) ^ 2 * τ + -↑π * I * (τ + 2 * z)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)

Tactic:
rw [h, abs_zero, ofReal_zero, zero_cpow hs₁, zero_cpow hs₃, div_zero, div_zero]

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (2 * ↑π * I * ↑a * -↑(n + 1))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + (1 - (1 + 1)))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)

Tactic:
← sub_sub,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑(n + 1)) + cexp (2 * ↑π * I * ↑a * -↑(n + 1))) * ↑(rexp (-π * ↑(n + 1) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + (1 - 1 - 1))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)))) =
    I *
      (cexp (-(↑π * I * z ^ 2 / τ)) *
        (-jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)))

Tactic:
congr 2

Goal state after:
case inr.e_a.e_a.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -(jacobiTheta₂' (z / τ) (-(1 / τ)) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ))) =
    -jacobiTheta₂' (z / τ) (-(1 / τ)) + z * jacobiTheta₂ (z / τ) (-(1 / τ)) * (2 * ↑π * I)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ oddKernel (-a) x = -oddKernel a x

Tactic:
by
  induction a using QuotientAddGroup.induction_on with
  | H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, oddKernel_def, jacobiTheta₂''_neg_left]

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
a : M
⊢ HasProd (fun p ↦ f ↑p) a ↔ HasProd (fun n ↦ if Prime n then f n else 1) a

Tactic:
by
  rw [ite_prime_eq_mulIndicator]; exact hasProd_subtype_iff_mulIndicator

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

Goal state before:
pp: case refine_1
s : ℂ
H : LSeriesSummable (fun n ↦ ↑(μ n)) s
⊢ 1 < s.re

pp: case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ ‖↑(μ n)‖ ≤ 1

Tactic:
· by_contra! h
    exact not_LSeriesSummable_moebius_at_one <| LSeriesSummable.of_re_le_re (by simpa) H

Goal state after:
case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ ‖↑(μ n)‖ ≤ 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun n_1 ↦ χ ↑n_1) ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ

Tactic:
← mul_one ↗χ

Goal state after:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun n_1 ↦ χ ↑n_1) * 1 ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
i : ℤ
⊢ 2 * ↑π * I * ↑a * ↑i = ↑(2 * π * a * ↑i) * I

Tactic:
by { push_cast; ring }

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (1 - s + 1) / 2 = ↑(3 / 2) - (s + 1) / 2

Tactic:
by { push_cast; ring }

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = ↑(2 * π * a * ↑n) * I

Tactic:
by { push_cast; ring }

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

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 = (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
congr 2

Goal state after:
case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = 1 / ↑|↑n + a| ^ s

case e_a.e_a
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + 1 - ↑a) ^ s = 1 / ↑|↑n + 1 - a| ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
by
  simp [cosZeta]

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

Goal state before:
pp: case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
intro f42

Goal state after:
case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
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) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0)
⊢ PythagoreanTriple (x0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (y0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k)))
    (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0 / ↑((x0 * ↑k).gcd (y0 * ↑k)))

Tactic:
have hk : (k : ℤ) ≠ 0 := by
    norm_cast
    rwa [pos_iff_ne_zero] at k0

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 * ↑k) (y0 * ↑k) (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k))) (y0 * ↑k / ↑((x0 * ↑k).gcd (y0 * ↑k)))
    (↑((x0 * ↑k).gcd (y0 * ↑k)) * z0 / ↑((x0 * ↑k).gcd (y0 * ↑k)))