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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 5 * n ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n - 1 ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n - 1 ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n + 1 ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 7 * n ∈ Set.Ici 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b

Tactic:
simpa using zmod_congr_of_sub_mem_span_aux n x a b ha hb

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
this✝¹ : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
this✝ : ∑ n ∈ Icc 1 N, b x (7 * n) ≤ ∑ n ∈ Icc 1 N, c x n
this : b x 1 = θ x
h1 : ψ x = b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - ↑x.zmodRepr ∈ nonunits ℤ_[p]

Tactic:
← IsLocalRing.mem_maximalIdeal

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x✝ x : ℝ
hx : x ∈ Set.Icc 2 x✝
this : x ≠ 0
⊢ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = -1

Tactic:
grind

Goal state after:
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)⁻¹ * ∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0) +
      ∫ (x : ℝ) in 2..x, (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log ↑x else 0) * ((log x ^ 2)⁻¹ * x⁻¹) =
    (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) / log x +
      ∫ (t : ℝ) in 2..x, (∑ a ∈ Icc 0 ⌊t⌋₊, if Nat.Prime a then log ↑a else 0) / (t * log t ^ 2)

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ log z ≠ 0

Tactic:
apply log_ne_zero_of_pos_of_ne_one

Goal state after:
case hx_pos
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ 0 < z

case hx
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
z : ℝ
left✝ : 2 ≤ z
right✝ : z ≤ x
this : z ≠ 0
⊢ z ≠ 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case funProp.discharger
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ ∀ x_1 ∈ Set.Icc 2 x, x_1 ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h✝ : x - ↑(x.appr n) = 0
⊢ x.appr n ≤ x.appr n

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ x ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁸ : EuclideanDomain R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain S
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra R K
inst✝¹² : IsFractionRing R K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : FiniteDimensional K L
inst✝⁹ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁸ : IsScalarTower R K L
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S L
ist : IsScalarTower R S L
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
⊢ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ ↑I ↔ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ I

Tactic:
rfl

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ ↑⋯.unit = ↑(⋯.unit ^ p ^ i)

Tactic:
rfl

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ↑↑⟨⋯.unit, ⋯⟩ = ↑(↑⟨⋯.unit, ⋯⟩ ^ aux g (p ^ (k + i)))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
have H₂ := aux_spec g (p ^ k)
    ⟨_, (h.isUnit_unit NeZero.out).mem_rootsOfUnity⟩

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ↑↑⟨⋯.unit, ⋯⟩ = ↑(↑⟨⋯.unit, ⋯⟩ ^ aux g (p ^ (k + i)))
H₂ : g ↑↑⟨⋯.unit, ⋯⟩ = ↑(↑⟨⋯.unit, ⋯⟩ ^ aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ x / log x ^ 2) =ᶠ[atTop] fun x ↦ x / log x ^ 2

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
this : log √x < log ↑p
⊢ log √x ≤ log ↑p + 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ),

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ ((leftMulMatrix (Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)).trace =
    (algebraMap R Rₘ) ((trace R S) a)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ f ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) x✝)) = (algebraMap (𝓞 L) L) (f₀ ((RingOfIntegers.basis K) x✝))

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (↑ringOfIntegersEquiv).symm 1 = ringOfIntegersEquiv.symm 1

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case s
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
| univ

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
| fun σ ↦ σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
rfl

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
| fun σ ↦ σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))
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
⊢ ofIntSeq 0 ⋯ = 0

Tactic:
rfl

Goal state after:
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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ ↑f (IsPrimitiveRoot.powerBasis K hμ).gen = ↑g (IsPrimitiveRoot.powerBasis K hμ).gen

Tactic:
AlgEquiv.coe_toAlgHom,

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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ f (IsPrimitiveRoot.powerBasis K hμ).gen = ↑g (IsPrimitiveRoot.powerBasis K hμ).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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ f (IsPrimitiveRoot.powerBasis K hμ).gen = ↑g (IsPrimitiveRoot.powerBasis K hμ).gen

Tactic:
AlgEquiv.coe_toAlgHom,

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
f g : L ≃ₐ[K] L
hfg : (autToPow K hμ) f = (autToPow K hμ) g
⊢ f (IsPrimitiveRoot.powerBasis K hμ).gen = g (IsPrimitiveRoot.powerBasis K hμ).gen
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝) x = (toZModPow n✝) x

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y

Tactic:
· rintro rfl _
    rfl

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g : R →+* ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝).comp g = (toZModPow n✝).comp g

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'

Tactic:
· rintro rfl _
    rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(a * a) - ↑1 = az a * az a - 1

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - d a1 * y * y = 1
⊢ ↑1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1

Tactic:
repeat' rw [Int.natCast_mul]; exact pn

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

Goal state before:
pp: case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).re = Int.ofNat a✝

Tactic:
rfl

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

Goal state before:
pp: case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).re = Int.negSucc a✝

Tactic:
rfl

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

Goal state before:
pp: case ofNat
d : ℤ
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).im = 0

Tactic:
rfl

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

Goal state before:
pp: case negSucc
d : ℤ
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).im = 0

Tactic:
rfl

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

Goal state before:
pp: case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

pp: case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Tactic:
· rintro ⟨x, rfl⟩
    simp

Goal state after:
case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
rfl

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

Goal state before:
pp: case ofNat.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.ofNat a✝¹)

Tactic:
rfl

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

Goal state before:
pp: case ofNat.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.ofNat a✝¹)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.negSucc a✝¹)

Tactic:
rfl

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

Goal state before:
pp: case negSucc.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.negSucc a✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
rfl

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

Goal state before:
pp: c d a b : ℕ
⊢ Nonnegg c d (-↑(a + 1)) ↑b ↔ SqLe (a + 1) d b c

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
a : α
⊢ (v ∘ f ⊗ t) (inl a) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inl a)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
b : γ
⊢ (v ∘ f ⊗ t) (inr b) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inr b)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
Nat.succ_mul,

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD yn a1 n ^ 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ (k * xn a1 n ^ k + xn a1 n ^ k) * yn a1 n [MOD yn a1 n ^ 3]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, p (v ⊗ t) = 0) ∧ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p ↦ p (v ⊗ n) = 0) pl
a : α
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inl a) = (v ⊗ m) (inl a)

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ : (∃ t, p (v ⊗ t) = 0) ∧ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
m : β → ℕ
hm : p (v ⊗ m) = 0
n : γ → ℕ
hn : List.Forall (fun p ↦ p (v ⊗ n) = 0) pl
b : β
⊢ ((v ⊗ m ⊗ n) ∘ (inl ⊗ inr ∘ inl)) (inr b) = (v ⊗ m) (inr b)

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
⊢ 1 / 2 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h₁ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.re + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.re =
    ↑(2 * a) * ↑(xn a1 (n + 1))
h₂ :
  { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) }.im + { re := ↑(xn a1 n), im := ↑(yn a1 n) }.im =
    ↑(2 * a) * ↑(yn a1 (n + 1))
⊢ xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD a - 1]

Tactic:
rw [yn_succ_succ, (by ring : n + 2 + n = 2 * (n + 1))]
      exact ((modEq_sub a1.le).mul_left 2).mul (yn_modEq_a_sub_one (n + 1))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD 2]

Tactic:
rfl

Goal state after: