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

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
by_cases h0 : n = 0

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

case neg
n : ℕ
h0 : ¬n = 0
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
⊢ ((μ.withDensity fun x ↦ ‖f x‖ₑ).withDensity fun x ↦ ‖‖f x‖⁻¹ • f x‖ₑ) = μ.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
← withDensity_mul₀ hf.aestronglyMeasurable.enorm

Goal state after:
case inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
⊢ μ.withDensity ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖‖f x‖⁻¹ • f x‖ₑ) = μ.withDensity fun x ↦ ‖f x‖ₑ

case inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
⊢ AEMeasurable (fun x ↦ ‖‖f x‖⁻¹ • f x‖ₑ) μ
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π (k + n) ≤ π k + φ a * (n / a + 1)

Tactic:
rw [primeCounting_eq_primeCounting'_succ]
  convert! primeCounting'_add_le h0 (Order.lt_add_one_iff.mpr h1) n using 2
  omega

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range (n + 1),
      (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) =
    (monomial n) ↑n + (monomial n) 1

Tactic:
sum_range_succ_comm

Goal state after:
n : ℕ
⊢ (∑ i ∈ range (n + 1 - n), ↑((n + 1 - n).choose i) * _root_.bernoulli i) • (monomial n) ↑((n + 1).choose n) +
      ∑ x ∈ range n,
        (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) =
    (monomial n) ↑n + (monomial n) 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ 1 -
      ∑ x ∈ range n,
        (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) =
    1

Tactic:
← sub_eq_zero,

Goal state after:
n : ℕ
⊢ 1 -
        ∑ x ∈ range n,
          (↑(n.choose x) / (↑n - ↑x + 1) * bernoulli' x - ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) -
      1 =
    0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n : ℕ
⊢ (↑n + 1) * ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x

Tactic:
simp_rw [mul_sum, ← mul_assoc]

Goal state after:
case succ
n : ℕ
⊢ ∑ x ∈ range n, (↑n + 1) * (↑(n.choose x) / (↑n - ↑x + 1)) * bernoulli' x =
    ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)

Tactic:
by
  have := bernoulli_comp_one_add_X n
  simpa using congr(Polynomial.eval x $this)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
this :
  (PowerSeries.mk fun p ↦ ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !

Tactic:
by
      rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
      rw [PowerSeries.ext_iff] at this
      simpa using this p

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p l : ℕ
inst✝ : Fact (Nat.Prime p)
v : ℕ
hv : v ∈ Ico 1 p
⊢ ¬p ∣ v

Tactic:
grind [not_dvd_of_pos_of_lt]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
⊢ pIntegral p (↑p ^ N / ↑M)

Tactic:
have hM_eq : (M : ℚ) = ↑(p ^ e) * ↑M' := by rw [← hdecomp]; simp

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ pIntegral p (↑p ^ N / ↑M)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ ↑n = 1

Tactic:
simp only [mem_filter, mem_Ioc] at hn

Goal state after:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
⊢ ↑n = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (∀ (x_1 : ℕ), 1 ≤ x_1 → x_1 ≤ n → Nat.Prime x_1 → ∀ (x_2 : ℕ), 1 ≤ x_2 → x_2 ≤ Nat.log x_1 n → ¬x_1 ^ x_2 = x) →
    ∀ (x_1 x_2 : ℕ), Nat.Prime x_1 → 0 < x_2 → ¬x_1 ^ x_2 = x

Tactic:
contrapose!

Goal state after:
case refine_2
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (∃ x_1 x_2, Nat.Prime x_1 ∧ 0 < x_2 ∧ x_1 ^ x_2 = x) →
    ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ n ∧ Nat.Prime x_1 ∧ ∃ x_2, 1 ≤ x_2 ∧ x_2 ≤ Nat.log x_1 n ∧ x_1 ^ x_2 = x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ ↑(Nat.log p n) * log ↑p ≤ log ↑n

Tactic:
refine le_log_of_pow_le (mod_cast (prime_of_mem_primesLE hp).pos) ?_

Goal state after:
case h
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ ↑p ^ Nat.log p n ≤ ↑n
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case b0
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
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ 0 < ↑(normBound abv bS)

Tactic:
· exact Int.cast_pos.mpr (normBound_pos abv bS)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n = ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n))

Tactic:
vonMangoldt_apply,

Goal state after:
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ n ∈ Ioc 0 ⌊x⌋₊, if IsPrimePow n then log ↑n.minFac else 0) = ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ |0| ≤ 2 * √x * log x

Tactic:
abs_zero

Goal state after:
case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ 0 ≤ 2 * √x * log x
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
set μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm

Goal state after:
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den

Tactic:
obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk
    rw [hT]
    have hT_int : pIntegral p T := Int.padicValuation_le_one p T
    have hR := pIntegral_faulhaber_sum hk fun m hm_pos hm_lt ↦
      Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)
    exact Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)

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 : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b

Tactic:
← sub_eq_zero,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a - ↑b = 0
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: 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
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * ⊥
⊢ False

Tactic:
Ideal.mul_bot

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
hJ : Ideal.span {(algebraMap R S) M} * ↑I = ⊥
⊢ False
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
⊢ ¬Ideal.span {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} = ⊥

Tactic:
Ideal.span_singleton_eq_bot

Goal state after:
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
⊢ ¬(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ (x - ↑(x.appr n)).valuation = (↑p ^ n * c).valuation

Tactic:
rw [hc]

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
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
obtain (h | h) := this.lt_or_eq

Goal state after:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 < Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
by
  rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,
    embeddingsMatrixReindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow]
  congr; ext i
  rw [← prod_pow]

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

Goal state before:
pp: case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist x ↑(x.appr n) < ε

Tactic:
rw [dist_eq_norm]

Goal state after:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ < ε
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 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
apply _root_.lt_trans _ hε'

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
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
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

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

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩

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 * (2 - 1) * (2 ^ k.succ * (2 - 1) - 1) / 2) = (-1) ^ (2 ^ k.succ * (2 - 1) / 2)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ (n + 1) ≤ xn a1 (n + 1)

Tactic:
by
    simp only [_root_.pow_succ, xn_succ]
    exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := -↑z, im := ↑w }).Nonneg

Tactic:
calc
          (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
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)
⊢ False

Tactic:
have co2 :=
        let co1 := co.mul_right co
        co1.mul_left co1

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)
⊢ False
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
⊢ j ≡ i [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
⊢ j ≡ j' [MOD 4 * n]
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ χ a * ∑ χ, χ a = ∑ χ, χ a

Tactic:
simp only [Finset.mul_sum, ← MulChar.mul_apply]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ i, (χ * i) a = ∑ χ, χ a
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0

Tactic:
have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers

Goal state after:
N k : ℕ
this✝ : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
n : ℕ
this : n ∈ k.smoothNumbers → n ≠ 0
⊢ n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
⊢ i = k

Tactic:
have iln : i ≤ n :=
              le_of_not_gt fun hin =>
                not_lt_of_ge (Nat.le_of_dvd vp (dvd_of_mul_left_dvd yv)) (strictMono_y a1 hin)

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
⊢ i = k
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 : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))

Tactic:
by
  rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
⊢ f ⍟ g = fun n ↦ ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2

Tactic:
ext n
  simpa [convolution, toArithmeticFunction] using
    Finset.sum_congr rfl fun p hp ↦ by simp [ne_zero_of_mem_divisorsAntidiagonal hp]

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

Goal state before:
pp: case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
        exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)

Goal state after: