mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
⊢ ⋃₀ range T.typesWith = univ

Tactic:
rw [← Set.univ_subset_iff]

Goal state after:
L : Language
T : L.Theory
α : Type u_1
⊢ univ ⊆ ⋃₀ range T.typesWith
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 * λ (2 ^ n) = φ (2 ^ n)

Tactic:
rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two]

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)

n : ℕ
hn : 3 ≤ n
⊢ 0 < n

n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))

Tactic:
rw [coeff_subst' hg, coeff_subst' hg]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
⊢ ∑ᶠ (d : ℕ), (coeff d) f • (coeff (n + 1)) (g ^ d) =
    ∑ᶠ (d : ℕ), (coeff d) ↑((trunc (m + 1)) f) • (coeff (n + 1)) (g ^ d)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
simp [isCyclic_units_two]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
mul_comm (_root_.bernoulli _) _,

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

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n ∣ n#

Tactic:
by
  have : (∏ p ∈ n.primeFactors, p) ∣ (∏ p ∈ range (n + 1) with p.Prime, p) :=
    Finset.prod_dvd_prod_of_subset _ _ _ (by grind [le_of_dvd])
  rwa [Nat.prod_primeFactors_of_squarefree hn] at this

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ≤ n
⊢ False

Tactic:
replace h1 : q ∣ n# := (minFac_prime (by lia)).dvd_primorial_iff.2 h1

Goal state after:
n : ℕ
hn : 2 < n
this : 3 ≤ n#
q : ℕ := (n# - 1).minFac
h1 : q ∣ n#
⊢ False
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ -(evalNegHom B * (1 - exp ℚ)) = X * 1

Tactic:
neg_eq_iff_eq_neg

Goal state after:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
h : B * (exp ℚ - 1) = X * exp ℚ
⊢ evalNegHom B * (1 - exp ℚ) = -(X * 1)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h
n : ℕ
ihn : ∀ m < n, m ≠ 0 → m# < 4 ^ m
hn : n ≠ 0
⊢ n# < 4 ^ n

Tactic:
rcases n with - | n; · grind
  rcases n.even_or_odd with ⟨m, rfl⟩ | ho
  · rcases m.eq_zero_or_pos with rfl | hm
    · decide
    calc
      (m + m + 1)# = (m + 1 + m)# := by rw [add_right_comm]
      _ ≤ (m + 1)# * choose (m + 1 + m) (m + 1) := primorial_add_le m.le_succ
      _ = (m + 1)# * choose (2 * m + 1) m := by rw [choose_symm_add, two_mul, add_right_comm]
      _ < 4 ^ (m + 1) * 4 ^ m :=
        Nat.mul_lt_mul_of_lt_of_le (ihn _ (by lia) (by lia)) (choose_middle_le_pow _) (by simp)
      _ ≤ 4 ^ (m + m + 1) := by rw [← pow_add, add_right_comm]
  · rcases Decidable.eq_or_ne n 1 with rfl | hn
    · decide
    · calc
        (n + 1)# = n# := primorial_succ hn ho
        _ < 4 ^ n := ihn n n.lt_succ_self (by grind)
        _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x ↦ log x + √(2 * x) * log (2 * x)

Tactic:
apply ConcaveOn.add

Goal state after:
case hf.hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) log

case hf.hg
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
⊢ ConcaveOn ℝ (Set.Ioi 0.5) fun x ↦ √(2 * x) * log (2 * x)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := ⋯
⊢ ∀ x ∈ range q.succ,
    bernoulli x / ↑x ! * (coeff (q - x + 1)) (exp ℚ ^ n) =
      bernoulli x * ↑((q + 1).choose x) * ↑n ^ (q + 1 - x) / ↑(q + 1)!

Tactic:
intro m h

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range q.succ
⊢ bernoulli m / ↑m ! * (coeff (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑((q + 1).choose m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!
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) / ↑p ! = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
div_eq_mul_inv,

Goal state after:
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) * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ.calc_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ 0 ≤ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖

Tactic:
exact mul_nonneg (norm_nonneg _) (sum_nonneg fun _ _ ↦ norm_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : 2 * ↑k - 2 * ↑m + 1 = ↑(d + 1)
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))

Tactic:
h_denom_rat,

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : 2 * ↑k - 2 * ↑m + 1 = ↑(d + 1)
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / ↑(d + 1))
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
simp only [mem_filter] at hn

Goal state after:
case refine_1
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊ ∧ Nat.Prime n
⊢ 1 < ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x = 0 ↔ x < 2

Tactic:
refine ⟨fun h₀ ↦ ?_, theta_eq_zero_of_lt_two⟩

Goal state after:
x : ℝ
h₀ : θ x = 0
⊢ x < 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑1 = 0

Tactic:
simp only [mul_one, cast_one, sub_self]

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
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (t : ℝ) in Set.Ioc 2 x, deriv (fun n ↦ (log n)⁻¹) t * ∑ k ∈ Icc 0 ⌊t⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

pp: case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume

Tactic:
← intervalIntegral.integral_of_le hx

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ (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)

case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (t : ℝ) in Set.Ioc 2 x, deriv log t * ∑ k ∈ Icc 0 ⌊t⌋₊, a k =
    ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

pp: case hint
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ IntegrableOn (deriv log) (Set.Icc 2 x) volume

Tactic:
← intervalIntegral.integral_of_le hx

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

case hint
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ IntegrableOn (deriv log) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:

Tactic:
_ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_

Goal state after:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ n + p ^ n * (p - 1)

case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ |θ t / (t * log t ^ 2)| ≤ log 4 * (1 / log t ^ 2)

Tactic:
calc |θ 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: 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, k ≠ 0 ∧ ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
    exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩

Goal state after:
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
⊢ nthHomSeq f_compat 1 ≈ 1

Tactic:
by
  intro ε hε
  change _ < _ at hε
  use 1
  intro j hj
  have : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow (by lia) hp_prime.1.one_lt⟩
  suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
  rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]

Goal state after:
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)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this✝ : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
this : (algebraMap ℤ ℚ) (r * r') = 1
⊢ r * r' = 1

Tactic:
rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this

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
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
⊢ (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun
      ((fun t ↦ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) x) =
    x

Tactic:
simp only [MonoidHom.toFun_eq_coe]
      generalize_proofs _ h
      have key := hζ.autToPow_spec K ((hζ.powerBasis K).equivOfMinpoly ((hμ x).powerBasis K) h)
      have := (hζ.powerBasis K).equivOfMinpoly_gen ((hμ x).powerBasis K) h
      rw [hζ.powerBasis_gen K] at this
      rw [this, IsPrimitiveRoot.powerBasis_gen] at key
      nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key
      simp only [← rootsOfUnity.coe_pow] at key
      replace key := rootsOfUnity.coe_injective key
      rw [pow_eq_pow_iff_modEq, ← Subgroup.orderOf_coe, ← orderOf_units, hζ.val_toRootsOfUnity_coe,
        ← (zeta_spec n K L).eq_orderOf, ← ZMod.natCast_eq_natCast_iff] at key
      simp only [ZMod.natCast_val, ZMod.cast_id', id] at key
      exact Units.ext key

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 : ℕ
⊢ (toZModPow n) (ofIntSeq f ⋯) = ↑(f n)

Tactic:
set x := PadicInt.ofIntSeq _ (isCauSeq_padicNorm_of_pow_dvd_sub f p hi)
  let s : PadicSeq p := ⟨(f ·), isCauSeq_padicNorm_of_pow_dvd_sub f p hi⟩
  have hs : x = Padic.mk s := rfl
  obtain ⟨e, he⟩ := Ideal.mem_span_singleton.mp (PadicInt.appr_spec n x)
  rw [sub_eq_iff_eq_add] at he
  obtain ⟨N, hN⟩ := padicNormE.defn s (ε := p ^ (-n : ℤ))
    (by simp only [zpow_neg, zpow_natCast, inv_pos]; exact_mod_cast Nat.pos_of_neZero _)
  replace hN := hN (N + n) (Nat.le_add_right N n)
  rw [← hs, he, ← Rat.cast_lt (K := ℝ)] at hN
  push_cast at hN
  simp only [← add_sub, s, Rat.cast_intCast, padicNormE.is_norm,
    ← Int.cast_natCast (R := ℚ_[p]) (x.appr n), ← Int.cast_sub] at hN
  have : ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ ≤ ↑p ^ (-n : ℤ) := by
    by_contra! H
    have H' : ‖(p ^ n * e : ℚ_[p])‖ < ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ := by
      refine LE.le.trans_lt ?_ H
      simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one
    rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN
    exact lt_asymm hN H
  rw [Padic.norm_int_le_pow_iff_dvd, ← Nat.cast_pow,
    ← ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_natCast] at this
  refine this.symm.trans ?_
  clear * - hi
  induction N with
  | zero => simp
  | succ N IH =>
    rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
    exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
simp_rw [add_apply, zero_apply, zero_add]

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

Tactic:
simpa using hζ

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = ↑d * y * y
⊢ x = 0 ∧ y = 0

Tactic:
rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.natCast_mul, ← mul_assoc] at h
  exact
    let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
    ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ False

Tactic:
by
  have t := (divides_sq_eq_zero e).left
  contradiction

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
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
⊢ IsPrimitiveRoot ζ (p ^ (0 + 1))

Tactic:
simpa using hζ

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

Tactic:
rw [Nat.mod_eq_of_lt this] at 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
⊢ a ≤ b
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
⊢ ∑ χ, χ a = if a = 1 then ↑n.totient else 0

Tactic:
by
  split_ifs with ha
  · simpa only [ha, map_one, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one,
      ← Nat.card_eq_fintype_card]
      using congrArg Nat.cast <| card_eq_totient_of_hasEnoughRootsOfUnity R n
  · exact sum_characters_eq_zero R ha

Goal state after:
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:
mem_factoredNumbers,

Goal state after:
s : Finset ℕ
m : ℕ
⊢ (m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s) ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → 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
this : List.filter (fun x ↦ decide (x = p)) m.primeFactorsList = List.filter (fun x ↦ decide (x ∉ s)) m.primeFactorsList
⊢ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ++ List.filter (fun x ↦ decide (x ∉ s)) m.primeFactorsList ~
    m.primeFactorsList

Tactic:
simp only [decide_not]

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
⊢ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ++ List.filter (fun x ↦ !decide (x ∈ s)) m.primeFactorsList ~
    m.primeFactorsList
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:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inl
n : ℕ
⊢ n ^ 0 = 1

Tactic:
exact _root_.pow_zero n

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

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 / ↑p.1 ^ s * term g s p.2

Tactic:
term_of_ne_zero hp₂,

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 / ↑p.1 ^ s * (g p.2 / ↑p.2 ^ s)
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case inl
f : ℕ → ℂ
s : ℂ
⊢ HasDerivAt (fun z ↦ term f z 0) (-term (logMul f) s 0) s

Tactic:
simp [hasDerivAt_const]

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

Goal state before:
pp: case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ f n / ↑n ^ z) (f n * (-log ↑n / ↑n ^ s)) s

Tactic:
div_eq_mul_inv,

Goal state after:
case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ f n * (↑n ^ z)⁻¹) (f n * (-log ↑n * (↑n ^ s)⁻¹)) s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b ↦ jacobiTheta₂'_term b z τ

Tactic:
rw [summable_jacobiTheta₂'_term_iff]

Goal state after:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im