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

Goal state before:
pp: case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
[

Goal state after:
case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖

Tactic:
[

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ log 4 * ‖∫ (t : ℝ) in 2..x, 1 / log t ^ 2‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:

Tactic:
|θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

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

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑(↑t ^ aux g n) = ↑(↑t ^ ↑(↑(aux g n)).val)

Tactic:
ZMod.val_intCast,

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑(↑t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: 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)
⊢ ∏ i, ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)) =
    (-1) ^ (n * (n - 1) / 2) * ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)

Tactic:
[

Goal state after:
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)
⊢ ∏ i, ∏ j > i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)) =
    (-1) ^ (n * (n - 1) / 2) * ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
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, ↑(#(Ioi x)) = ↑(n * (n - 1) / 2)

Tactic:
[

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, ↑(#(Ioi x)) = ↑(n * (n - 1) / 2)
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
i j : ι
⊢ traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
i j : ι
⊢ traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j
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)
⊢ discr ℚ ⇑b = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2 * discr ℚ ⇑(b.reindex (b.indexEquiv b'))

Tactic:
← one_mul (discr ℚ b),

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)
⊢ 1 * discr ℚ ⇑b = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2 * discr ℚ ⇑(b.reindex (b.indexEquiv b'))
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 ∈ ⊥
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
← B.basis.sum_repr z,

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 ∈ ⊥
⊢ discr K ⇑B.basis • ∑ i, (B.basis.repr z) i • B.basis i ∈ R[B.gen]
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)
⊢ (fromZetaAut hμ h) (zeta n K L) = μ

Tactic:
[

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)
⊢ (fromZetaAut hμ h) (zeta n K L) = μ
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inl.succ
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)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ ((n✝ + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ ((n✝ + 1).succ + 1))
hirr : Irreducible (cyclotomic (2 ^ ((n✝ + 1).succ + 1)) K)
hk : 2 ^ ((n✝ + 1).succ + 1) ≠ 2
hne : NeZero ↑(2 ^ ((n✝ + 1).succ + 1))
hp2 : 2 = 2 → (n✝ + 1).succ ≠ 0
⊢ (-1) ^ (2 ^ (n✝ + 1) * (2 * 2 ^ (n✝ + 1) - 1)) = (-1) ^ 2 ^ (n✝ + 1)

Tactic:
[

Goal state after:
case e_a.inl.succ
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)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ ((n✝ + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ ((n✝ + 1).succ + 1))
hirr : Irreducible (cyclotomic (2 ^ ((n✝ + 1).succ + 1)) K)
hk : 2 ^ ((n✝ + 1).succ + 1) ≠ 2
hne : NeZero ↑(2 ^ ((n✝ + 1).succ + 1))
hp2 : 2 = 2 → (n✝ + 1).succ ≠ 0
⊢ (-1) ^ (2 ^ (n✝ + 1) * (2 * 2 ^ (n✝ + 1) - 1)) = (-1) ^ 2 ^ (n✝ + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ n * n + 1

Tactic:
this

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ a * a
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ + x✝² + x✝¹) x✝ = (x✝³ + (x✝² + x✝¹)) x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ + x✝² + x✝¹) x✝ = (x✝³ + (x✝² + x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 + x✝¹) x✝ = x✝¹ x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 + x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ + 0) x✝ = x✝¹ x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ + 0) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (-x✝¹ + x✝¹) x✝ = 0 x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (-x✝¹ + x✝¹) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² + x✝¹) x✝ = (x✝¹ + x✝²) x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² + x✝¹) x✝ = (x✝¹ + x✝²) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * x✝² * x✝¹) x✝ = (x✝³ * (x✝² * x✝¹)) x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * x✝² * x✝¹) x✝ = (x✝³ * (x✝² * x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (1 * x✝¹) x✝ = x✝¹ x✝

Tactic:
rw [mul_apply, one_apply, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 0 * x✝ = 0

Tactic:
ext; rw [mul_apply, zero_apply, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * (x✝² + x✝¹)) x✝ = (x✝³ * x✝² + x✝³ * x✝¹) x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * (x✝² + x✝¹)) x✝ = (x✝³ * x✝² + x✝³ * x✝¹) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
⊢ p ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) = 0

Tactic:
this

Goal state after:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
this : (v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f) = v ⊗ t
⊢ p (v ⊗ t) = 0
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
⊢ p (v ⊗ t ∘ f) = 0

Tactic:
this

Goal state after:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : γ → ℕ
ht : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
this : v ⊗ t ∘ f = (v ⊗ t) ∘ (inl ⊗ inr ∘ f)
⊢ p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
Int.isUnit_iff_natAbs_eq,

Goal state after:
d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ z.norm.natAbs = 1
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)
    rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_natCast,
      derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_natCast,
      hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H
    replace H := congr_arg (fun P => aeval ζ P) H
    simp only [aeval_add, aeval_mul, minpoly.aeval, zero_mul, add_zero, aeval_natCast,
      map_sub, aeval_one, aeval_X_pow] at H
    replace H := congr_arg (Algebra.norm K) H
    have hnorm : (norm K) (ζ ^ p ^ k - 1) = (p : K) ^ p ^ k := by
      by_cases hp : p = 2
      · exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
      · exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp
    rw [map_mul, hnorm, map_mul, ← map_natCast (algebraMap K L),
      Algebra.norm_algebraMap, finrank L hirr, ← succ_eq_add_one,
      totient_prime_pow hp.out (succ_pos k), Nat.sub_one, Nat.pred_succ] at H
    rw [← hζ.minpoly_eq_cyclotomic_of_irreducible hirr, map_pow, hζ.norm_eq_one hk hirr, one_pow,
      mul_one, cast_pow, ← pow_mul, ← mul_assoc, mul_comm (k + 1), mul_assoc] at H
    have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)
    rw [← succ_pred_eq_of_pos this, mul_succ, pow_add _ _ (p ^ k)] at H
    replace H := (mul_left_inj' fun h => ?_).1 H
    · simp only [H, mul_comm _ (k + 1)]; norm_cast
    · have := hne.1
      rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by lia)] at this
      exact absurd (eq_zero_of_pow_eq_zero h) this

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

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Tactic:
this

Goal state after:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ (↑x * a + sqrtd * (↑y * a)).Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
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
⊢ discr K ((fun i ↦ ζ ^ ↑i) ∘ ⇑e.symm) = 1

Tactic:
[

Goal state after:
case pos
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
⊢ discr K ((fun i ↦ ζ ^ ↑i) ∘ ⇑e.symm) = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Tactic:
exact
    (dvd_mul_right _ _).modEq_zero_nat.add
      (Int.natCast_dvd_natCast.1 <| by simpa [xz, yz] using h1).modEq_zero_nat

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

Goal state before:
pp: 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 = (minpoly K ζ).natDegree

Tactic:
this

Goal state after:
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 = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b

Tactic:
[

Goal state after:
d : ℕ
a b : ℤ√↑d
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ m * m

Tactic:
this

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a : ℤ√d
⊢ a.norm = 1 ↔ a ∈ unitary (ℤ√d)

Tactic:
rw [Unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]
  norm_cast

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Tactic:
have hfu := fun m : ℤ => mul_lt_of_lt_one_left hn <| fract_lt_one (ξ * ↑m)

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
hu : IsUnit a
ha : hu.unit = 1
⊢ a = 1

Tactic:
← hu.unit_spec,

Goal state after:
case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
hu : IsUnit a
ha : hu.unit = 1
⊢ ↑hu.unit = 1
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 % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ a ≤ b

Tactic:
← ba

Goal state after:
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 % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ b % u ≤ b
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
[

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s

Tactic:
[

Goal state after:
s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
have hp' := pow_ne_zero e hp.ne_zero

Goal state after:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod

Tactic:
have : m.primeFactorsList.filter (· = p) = m.primeFactorsList.filter (· ∉ s) :=
      filter_congr <| by grind

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
this : List.filter (fun x ↦ decide (x = p)) m.primeFactorsList = List.filter (fun x ↦ decide (x ∉ s)) m.primeFactorsList
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod =
    m.primeFactorsList.prod
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow

Tactic:
[

Goal state after:
n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow