mathlib-initiative/mathlib-tactics huggingface dataset:
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) i j)
⊢ ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)

Tactic:
intro i

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) i j)
i : ι'
⊢ ∀ (j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑(padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n))) < ↑ε'

Tactic:
norm_cast

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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n)) < ε'
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf (zeta n K L)]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x

Tactic:
← (zeta_spec n K L).eq_orderOf,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD n]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
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
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
⊢ ∑ x, discr K ⇑B.basis • (B.basis.repr z) x • B.basis x ∈ R[B.gen]

Tactic:
refine Subalgebra.sum_mem _ fun i _ => ?_

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
i : Fin B.dim
x✝ : i ∈ univ
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = z

Tactic:
by
  change _ = RingHom.id _ z
  rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
  intro; rw [RingHom.comp_id]

Goal state after:
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
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
⊢ ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

Tactic:
intro i

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: 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
⊢ (-1) ^ (φ (p ^ (k + 1)) * (φ (p ^ (k + 1)) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
totient_prime_pow hp.out (succ_pos k),

Goal state after:
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
⊢ (-1) ^ (p ^ (k.succ - 1) * (p - 1) * (p ^ (k.succ - 1) * (p - 1) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) =
    (-1) ^ (p ^ (k.succ - 1) * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

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

Tactic:
succ_sub_succ_eq_sub,

Goal state after:
case e_a.inl
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * (1 - 0) * (2 ^ k.succ * (1 - 0) - 1) / 2) = (-1) ^ (2 ^ k.succ * (1 - 0) / 2)
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
H :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ k.succ) ^ φ (p ^ k.succ) * (Algebra.norm K) (ζ ^ (p ^ k.succ - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
totient_prime_pow hp.out (succ_pos 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 :
  (Algebra.norm K) ((aeval ζ) (derivative (minpoly K ζ))) * ↑p ^ p ^ k =
    ↑(p ^ k.succ) ^ (p ^ (k.succ - 1) * (p - 1)) * (Algebra.norm K) (ζ ^ (p ^ k.succ - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case const
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
n✝ : ℤ
⊢ C ⟨fun x ↦ n✝, ⋯⟩

Tactic:
| const =>

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.refine_2
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
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
H : (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * (k.succ * (p - 1)).pred)
⊢ ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) = ↑p ^ (p ^ k * ((k + 1) * (p - 1) - 1))

Tactic:
norm_cast

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

Goal state before:
pp: d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ z.norm.natAbs = 1

Tactic:
norm_eq_one_iff

Goal state after:
d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ IsUnit z
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ (-1) ^ ↑(e.symm i) = 1

Tactic:
suffices (e.symm i : ℕ) = 0 by simp [this]

Goal state after:
case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ ↑a.norm = 1

Tactic:
norm_cast

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

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

Tactic:
norm_cast

Goal state after:
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✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
⊢ (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ x ⊗ t) = 0

Tactic:
by
          simp only [Poly.map_apply]
          rw [show (v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ x) ⊗ t from
            funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl]
          exact ht

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

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : (MonoidHom.domRestrictHom N.units Rˣ) ψ = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ ((domRestrictHom N R) (ofUnitHom ψ)) ↑x✝ = χ ↑x✝

Tactic:
rw [MonoidHom.domRestrictHom_apply] at hψ

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
χ : MulChar (↥N) R
ψ : Mˣ →* Rˣ
hψ : ψ.domRestrict N.units = χ.toUnitHom.comp ↑N.unitsEquivUnitsType
x✝ : (↥N)ˣ
⊢ ((domRestrictHom N R) (ofUnitHom ψ)) ↑x✝ = χ ↑x✝
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num|

Tactic:
norm_cast

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - ↑ξ.den * q.num|
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Tactic:
norm_cast

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

Goal state before:
pp: v : ℤ
hv : 0 < v
⊢ 0 < 2 * ↑v - 1

Tactic:
norm_cast

Goal state after:
v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 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' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ 1 ≤ |↑⌊ξ⌋ * ↑v - ↑u|

Tactic:
norm_cast

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

Goal state before:
pp: case ha
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 0 ≤ ↑a - ↑y

Tactic:
norm_cast

Goal state after:
case ha
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 0 ≤ a - y
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case h
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 1 ≤ ↑y

Tactic:
norm_cast

Goal state after:
case h
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ 1 ≤ y
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < LSeries a ↑x

Tactic:
by
  rw [LSeries]
  refine Summable.tsum_pos ?_ (fun n ↦ term_nonneg (ha₀ n) x) 1 <| term_pos one_ne_zero ha₁ x
  exact LSeriesSummable_of_abscissaOfAbsConv_lt_re <| by simpa only [ofReal_re] using hx

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

Goal state before:
pp: case refine_2
ξ : ℝ
q : ℚ
h : |ξ - ↑↑q.num| < 1 / (2 * ↑(↑q.num).den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num

Tactic:
simpa only [Rat.den_intCast, Nat.cast_one, one_pow, mul_one] using! (abs_lt.mp h).1

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

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ ↑q.num / ↑q.den = ↑(↑q.num / ↑q.den)

Tactic:
norm_cast

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

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * (↑n * rexp (-π * t) ^ n)

Tactic:
rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = ↑n * rexp (↑n * (-π * t) + -π * a ^ 2 * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
a' : ℝ
⊢ ContinuousOn (evenKernel ↑a') (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
  simp only [evenKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
  exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
    (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

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
⊢ Tendsto (fun s ↦ (s - ↑P.k) • P.Λ₀ s - (s - ↑P.k) • (1 / s) • P.f₀ - (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀)
    (𝓝[≠] ↑P.k) (𝓝 (P.ε • P.g₀))

Tactic:
(by simp : 𝓝 (P.ε • P.g₀) = 𝓝 (0 - 0 - -P.ε • P.g₀))

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • P.Λ₀ s - (s - ↑P.k) • (1 / s) • P.f₀ - (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀)
    (𝓝[≠] ↑P.k) (𝓝 (0 - 0 - -P.ε • P.g₀))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a) (I * ↑x)) x

Tactic:
have h := continuousAt_jacobiTheta₂' a (by rwa [I_mul_im, ofReal_re])

Goal state after:
a x : ℝ
hx : x ∈ Ioi 0
h : ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (↑a, I * ↑x)
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a) (I * ↑x)) x
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ Function.update (fun s ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) = hurwitzZetaEven 0

Tactic:
hurwitzZetaEven,

Goal state after:
⊢ Function.update (fun s ↦ completedCosZeta 0 s / s.Gammaℝ) 0 (-1 / 2) =
    Function.update (fun s ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0 (if True then -1 / 2 else 0)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: ⊢ hurwitzZetaEven 0 0 = -1 / 2

Tactic:
hurwitzZetaEven,

Goal state after:
⊢ Function.update (fun s ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0 (if True then -1 / 2 else 0) 0 = -1 / 2
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ hurwitzZetaEven 0 s = completedRiemannZeta s / s.Gammaℝ

Tactic:
hurwitzZetaEven,

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven 0 s / s.Gammaℝ) 0 (if 0 = 0 then -1 / 2 else 0) s =
    completedRiemannZeta s / s.Gammaℝ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Tactic:
have (s : _) : completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
      ((if a = 0 then 1 else 0) - (if b = 0 then 1 else 0)) / s := by
    simp_rw [completedHurwitzZetaEven_eq, sub_div]
    abel

Goal state after:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
h0 : (0 ^ k)⁻¹ = 0
⊢ 2 * riemannZeta ↑k = (↑0 ^ k)⁻¹ + 2 • ∑' (n : ℕ+), (↑↑↑n ^ k)⁻¹

Tactic:
norm_cast

Goal state after:
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
h0 : (0 ^ k)⁻¹ = 0
⊢ 2 * riemannZeta ↑k = (↑(0 ^ k))⁻¹ + 2 • ∑' (n : ℕ+), (↑↑(n ^ k))⁻¹
Module: Mathlib.NumberTheory.LSeries.Dirichlet

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

Tactic:
norm_cast

Goal state after:
case refine_2
s : ℂ
n : ℕ
x✝ : n ≠ 0
⊢ |μ n| ≤ 1
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
m : ℕ := 2 ^ k.primesBelow.card
N₀ : ℕ := 2 * m ^ 2
hN₀ : N₀ = 2 * m ^ 2
S : ℝ := ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p
⊢ ↑m * ↑(2 * N₀).sqrt + ↑(2 * N₀) * ∑ p ∈ (2 * N₀).succ.primesBelow \ k.primesBelow, 1 / ↑p ≤
    ↑m * ↑(2 * N₀).sqrt + 2 * ↑N₀ * S

Tactic:
norm_cast

Goal state after: