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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.346 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.346 n, c k
⊢ t ∈ Set.Icc (↑n) (↑n + 1) → g t * ?m.294 = g t * ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
ht

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.346 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.346 n, c k
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ g t * ?m.294 = g t * ∑ k ∈ Icc m ⌊t⌋₊, c k
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case hfin
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1 + ↑p ^ (n + 1) * ↑p ^ m * (↑a + ↑p * y)
⊢ (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1

Tactic:
rw [hy, ← pow_add, ← Nat.cast_pow]

Goal state after:
case hfin
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1 + ↑p ^ (n + 1) * ↑p ^ m * (↑a + ↑p * y)
⊢ 1 + ↑(p ^ (n + 1 + m)) * (↑a + ↑p * y) = 1
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1)) (f * g) * (↑(n i) + 1) = (coeff n) (f • pderivFun i g) + (coeff n) (g • pderivFun i f)

Tactic:
← coeff_trunc_mul_trunc_eq_coeff_mul _ _ _ h₂,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ MvPolynomial.coeff (n + single i 1)
        ((trunc R (n + single i 1 + single i 1)) f * (trunc R (n + single i 1 + single i 1)) g) *
      (↑(n i) + 1) =
    (coeff n) (f • pderivFun i g) + (coeff n) (g • pderivFun i f)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ IsCyclic (ZMod (2 ^ n))ˣ ↔ n ≤ 2

Tactic:
match n with
  | 0 => simp [isCyclic_units_one]
  | 1 => simp [isCyclic_units_prime Nat.prime_two]
  | 2 => simp [isCyclic_units_four]
  | n + 3 =>
    simp only [Nat.reduceLeDiff, iff_false]
    intro H
    apply not_isCyclic_units_eight
    have h : 2 ^ 3 ∣ 2 ^ (n + 3) := pow_dvd_pow _ (by lia)
    exact isCyclic_of_surjective _ (unitsMap_surjective h)

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (False ∨ m = 2) ∨ n = 1 ∨ n = 2
⊢ False

Tactic:
hn1,

Goal state after:
m n : ℕ
hm : Odd m
hm1 : m ≠ 1
hn : Odd n
hn1 : n ≠ 1
hmn : m.Coprime n
x✝¹ : NeZero m
x✝ : NeZero n
e : (ZMod (m * n))ˣ ≃* (ZMod m)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
h : (False ∨ m = 2) ∨ False ∨ n = 2
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!) = ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
← map_natCast (algebraMap ℚ A) (n.choose x),

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ (algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!) =
    (algebraMap ℚ A) ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n.primeFactors ⊆ {p ∈ range (n + 1) | Nat.Prime p}

Tactic:
grind [le_of_dvd]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
⊢ ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))

Tactic:
intro x h5

Goal state after:
x✝ : ℝ
x_large : 512 ≤ x✝
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
x : ℝ
h5 : 0 < x
⊢ f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
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)!
hexp : exp ℚ - 1 ≠ 0
⊢ (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)!

Tactic:
have h_r : exp ℚ ^ n - 1 = X * mk fun p => coeff (p + 1) (exp ℚ ^ n) := by
      have h_const : C (constantCoeff (exp ℚ ^ n)) = 1 := by simp
      rw [← h_const, sub_const_eq_X_mul_shift]

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)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p ↦ (coeff (p + 1)) (exp ℚ ^ n)
⊢ (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)!
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case hf
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
obtain h | h : ¬ x.Prime ∨ x ≤ n := by simpa [imp_iff_not_or, hx.not_gt] using no_prime x

Goal state after:
case hf.inl
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : ¬Nat.Prime x
⊢ x ^ n.centralBinom.factorization x = 1

case hf.inr
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : p ^ k ∈ Icc 1 n
⊢ ∃ x, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k

Tactic:
simp only [mem_Icc] at hx

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
⊢ ∃ x, 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ x_1, 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∀ (p : ℕ), Nat.Prime p → (n.choose k).factorization p ≤ n.lcmUpto.factorization p

Tactic:
intro p hp

Goal state after:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
⊢ (n.choose k).factorization p ≤ n.lcmUpto.factorization p
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 ℤ
I : ↥(Ideal S)⁰
⊢ ∃ b, ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → b ≤ z

Tactic:
by
      use 0
      rintro _ ⟨b, _, _, rfl⟩
      apply abv.nonneg

Goal state after:
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 ℤ
I : ↥(Ideal S)⁰
⊢ ∃ z, ∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z

Tactic:
obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)
      exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
sum_PrimePow_eq_sum_sum' _ hx hN

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

Goal state before:
pp: case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑n))| ≤ 2 * √x * log x

Tactic:
apply le_trans <| abs_sum_le_sum_abs ..

Goal state after:
case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ (1 / ↑i))| ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ (1 / ↑x_1)) ≤ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x

pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x

Tactic:
· gcongr with i hi
    apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))
    rw [sqrt_eq_rpow]
    gcongr; simp_all

Goal state after:
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    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
⊢ 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, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * (N + 1) - 1) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))

Tactic:
rw [show 6 * (N + 1) - 1 = 6 * N + 5 by lia]

Goal state after:
case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    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
⊢ 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, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * N + 5) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
⊢ ∀ (a : F[X]), (algebraMap F[X] ↥(ringOfIntegers F K)) a = 0 → a = 0

Tactic:
intro p hp

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
hinj : Function.Injective ⇑(algebraMap F[X] K)
p : F[X]
hp : (algebraMap F[X] ↥(ringOfIntegers F K)) p = 0
⊢ p = 0
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 := ⋯
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
⊢ Ideal.span {b} ≤ ↑I

Tactic:
Ideal.span_le,

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
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
⊢ {b} ⊆ ↑↑I
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
⊢ Ideal.span {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} ≤ I ↔ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ I

Tactic:
Ideal.span_le,

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
I : Ideal S
⊢ {(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m)} ⊆ ↑I ↔ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ∈ I
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case pos
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
⊢ ↑p ^ (n + 1) ∣ x - ↑(x.appr n)

Tactic:
rw [h]
      apply dvd_zero

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✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
f : (S ⧸ (↑R (Algebra.linearMap S L)).ker) ≃ₗ[R] S := ⋯.mpr (⊥.quotEquivOfEqBot ⋯)
bS : Basis (Fin n) R S := b.map ((↑R (Algebra.linearMap S L)).quotKerEquivRange.symm ≪≫ₗ f)
⊢ Fintype (ClassGroup S)

Tactic:
have : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L

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✝ : IsIntegralClosure S R L
this✝³ : DecidableEq L := Classical.decEq L
this✝² : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝¹ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this✝ : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
f : (S ⧸ (↑R (Algebra.linearMap S L)).ker) ≃ₗ[R] S := ⋯.mpr (⊥.quotEquivOfEqBot ⋯)
bS : Basis (Fin n) R S := b.map ((↑R (Algebra.linearMap S L)).quotKerEquivRange.symm ≪≫ₗ f)
this : Algebra.IsIntegral R S
⊢ Fintype (ClassGroup S)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
t : ℝ
⊢ t ∈ Set.uIcc 2 x → (fun x ↦ |1 / log x ^ 2|) t = (fun t ↦ 1 / log t ^ 2) t

Tactic:
ht

Goal state after:
x : ℝ
hx : 4 ≤ x
t : ℝ
ht : t ∈ Set.uIcc 2 x
⊢ (fun x ↦ |1 / log x ^ 2|) t = (fun t ↦ 1 / log t ^ 2) t
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
norm_eq_abs

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

Goal state before:
pp: ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ discr K ⇑b ≠ 0

Tactic:
by
  rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]
  exact traceForm_nondegenerate _ _

Goal state after:
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) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
t : Lˣ
⊢ t ∈ rootsOfUnity (p ^ k) L → ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑t = ↑t ^ ZMod.val 1

Tactic:
ht

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)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
t : Lˣ
ht : t ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑t = ↑t ^ ZMod.val 1
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
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p 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 s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
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
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = (algebraMap ℤ ℚ) (Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))

Tactic:
← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L

Goal state after:
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
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) =
    Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))
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
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p 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 s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε