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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ∃ J, mk0 I = mk0 J ∧ (algebraMap R S) M ∈ ↑J

Tactic:
refine ⟨⟨J, ?_⟩, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ J ∈ (Ideal S)⁰

case refine_2
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ mk0 I = mk0 ⟨J, ?refine_1⟩

case refine_3
R : Type u_1
S : Type u_2
inst✝⁹ : EuclideanDomain R
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝³ : Infinite R
inst✝² : DecidableEq R
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ (algebraMap R S) M ∈ ↑⟨J, ?refine_1⟩
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ (↑x).zmodRepr ≠ 0

Tactic:
ne_eq,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ ¬(↑x).zmodRepr = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
int_deriv :
  ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u = ∫ (u : ℝ) in 2..x, f u * -(u * log u ^ 2)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
int_deriv

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
int_deriv :
  ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u = ∫ (u : ℝ) in 2..x, f u * -(u * log u ^ 2)⁻¹
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) * -(u * log u ^ 2)⁻¹ =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
int_deriv : ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ log x) u * f u = ∫ (u : ℝ) in 2..x, f u / u
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t

Tactic:
int_deriv

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
int_deriv : ∀ (f : ℝ → ℝ), ∫ (u : ℝ) in 2..x, deriv (fun x ↦ log x) u * f u = ∫ (u : ℝ) in 2..x, f u / u
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) / u =
    ↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) * log x -
      ∫ (t : ℝ) in 2..x, ↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) / t
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Tactic:
by
      convert! appr_spec n x
      simp only [this, sub_zero, cast_zero]

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

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

Tactic:
toFun_spec' g ht

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ (toFun n g).val = ↑t ^ (↑((modularCyclotomicCharacter L hn) g)).val
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ ↑(π ⌊x⌋₊)

Tactic:
div_le_iff₀ (log_pos hx),

Goal state after:
x : ℝ
hx : 1 < x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ↑(π ⌊x⌋₊) * log x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
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
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) ≤ ↑p ^ (-↑k)

Tactic:
beta_reduce

Goal state after:
case h
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
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p (↑(nthHom f r j) - ↑(nthHom f r k)) ≤ ↑p ^ (-↑k)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ ∀ x ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup),
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
      Metric.ball 1 ε

Tactic:
intro σ

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
⊢ σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup) →
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) σ ∈
      Metric.ball 1 ε
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)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
⊢ ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E

Tactic:
intro σ

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
σ : L →ₐ[K] E
⊢ σ pb.gen ∈ (minpoly K pb.gen).aroots E
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ (𝓞 K)
b₀ : Basis ι ℤ (𝓞 K) := (RingOfIntegers.basis K).reindex ((RingOfIntegers.basis K).indexEquiv b)
⊢ Algebra.discr ℤ ⇑b = discr K

Tactic:
rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.refine_3
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
hroots :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
a : L →ₐ[K] E
b : E
hba✝ :
  b ≠ a pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
hba :
  b ≠ b ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
ha : a = pb.lift b ⋯
⊢ False

Tactic:
exact hba.1 rfl

Goal state after:
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
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
⊢ 0 < ↑p ^ (-↑n)

Tactic:
simp only [zpow_neg, zpow_natCast, inv_pos]; exact_mod_cast Nat.pos_of_neZero _

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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

Tactic:
← congr_fun cramer 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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ (traceMatrix K ⇑B.basis).cramer (fun i ↦ (trace K L) (z * B.basis i)) i ∈ ⊥
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
ext; rw [mul_apply, one_apply, mul_one]

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

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

Tactic:
have := hne.1

Goal state after:
case e_a.refine_1
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 (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ↑(p ^ (k + 1)) ≠ 0
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case zero
a : ℕ
a1 : 1 < a
n : ℕ
hx : xn a1 (n * 0) ≡ xn a1 n ^ 0 [MOD yn a1 n ^ 2]
hy : yn a1 (n * 0) ≡ 0 * xn a1 n ^ (0 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * 0) * xn a1 n + d a1 * yn a1 (n * 0) * yn a1 n ≡ xn a1 n ^ 0 * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ 0 * xn a1 n ^ (0 - 1) * yn a1 n * xn a1 n = 0 * xn a1 n ^ 0 * yn a1 n

Tactic:
simp [_root_.pow_succ]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp [_root_.pow_succ]

Goal state after:
case succ
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    yn a1 n ^ 2]
⊢ (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n
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.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 n * yn a1 n ∣ yn a1 n ^ 3

Tactic:
simp [_root_.pow_succ]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ yn a1 n * yn a1 n ∣ yn a1 n ^ 3

Tactic:
simp [_root_.pow_succ]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 2 * n ≤ 2 * n

Tactic:
by rw [Nat.succ_mul]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ lin)]

Goal state after:
case refl.inl
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
lin : i < n
⊢ xn a1 (n - 1) + xn a1 i < xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
ji

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
⊢ 4 * n ≡ 0 [MOD 4 * n]
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m n : ℕ
hm : m ∈ factoredNumbers s
hn : n ∈ factoredNumbers s
⊢ m * n ∈ factoredNumbers s

Tactic:
have hm' := primeFactors_subset_of_mem_factoredNumbers hm
  have hn' := primeFactors_subset_of_mem_factoredNumbers hn
  exact mem_factoredNumbers_of_primeFactors_subset (mul_ne_zero hm.1 hn.1)
    <| primeFactors_mul hm.1 hn.1 ▸ Finset.union_subset hm' hn'

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n : ℕ
⊢ n.smoothNumbers = factoredNumbers n.primesBelow

Tactic:
rw [smoothNumbers_eq_factoredNumbers]
  refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter
  simp_rw [mem_factoredNumbers'] at hm ⊢
  exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ ∀ (p : ℕ), Prime p → p ∣ m → p < n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers', Finset.mem_range]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
⊢ LSeriesSummable f s

Tactic:
obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
    simpa [abscissaOfAbsConv, sInf_lt_iff] using hs
  exact hy.of_re_le_re <| ofReal_re y ▸ hys.le

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ HasProd (fun p ↦ ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)

Tactic:
change HasProd (F ∘ Subtype.val (p := (· ∈ {x | Nat.Prime x}))) _

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ HasProd (F ∘ Subtype.val) (∑' (n : ℕ), f n)
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p ↦ p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
show (fun p : ℕ × ℕ ↦ p.1 * p.2) ⁻¹' {n} = n.divisorsAntidiagonal by ext; simp [hn],

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑↑n.divisorsAntidiagonal), term f s (↑b).1 * term g s (↑b).2
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
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

Tactic:
div_one

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 = ξ.convergent n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

pp: case refine_2
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
⊢ 0 < τ.im

Tactic:
· refine (summable_pow_mul_jacobiTheta₂_term_bound |im z| hτ 0).of_norm_bounded ?_
    simpa only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl

Goal state after:
case refine_2
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
⊢ 0 < τ.im
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ 1 / 1 < x

Tactic:
div_one

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
⊢ 1 < x
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
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]
    rw [f_modif, Pi.add_apply, indicator_of_notMem (notMem_Ioi.mpr this.le),
      zero_add, indicator_of_mem (mem_Ioo.mpr ⟨div_pos one_pos hx, this⟩), g_modif, Pi.add_apply,
      indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem
      (notMem_Ioo_of_ge hx'.le), add_zero, P.h_feq _ hx, smul_sub]
    simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]

Goal state after: