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

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑(x.1 + x.2)! =
    ↑((x.1 + x.2)! / (x.1! * x.2!)) / (↑x.2 + 1) * bernoulli x.1

Tactic:
cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑(x.1 + x.2)! =
    ↑(x.1 + x.2)! / ↑(x.1! * x.2!) / (↑x.2 + 1) * bernoulli x.1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
⊢ ∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i

Tactic:
have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ :=
      fun r => by rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]

Goal state after:
case succ
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
⊢ ∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ (d + 1).factorization p ≤ d - 1

Tactic:
apply Nat.factorization_le_of_le_pow
    have hp2 := (Fact.out : p.Prime).two_le
    suffices ∀ n : ℕ, n ≥ 2 → ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1) from this d hd hcase
    intro n hn hne'
    induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..

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 ℤ
ι : 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 : ι
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
have him : (Finset.univ.image fun k => abv (bS.repr a k)).Nonempty :=
    ⟨_, Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩⟩

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
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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ log x / log 2

Tactic:
trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n.lcmUpto ≠ 0

Tactic:
simp [lcmUpto_ne_zero]

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

Goal state before:
pp: case refine_1.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A 0 % b)) < cardPowDegree b • ε
⊢ False

Tactic:
← not_le,

Goal state after:
case refine_1.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A 0 % b))
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x✝ x : ℝ
hx : x ∈ Set.Icc 2 x✝
this : x ≠ 0
⊢ ContinuousAt (fun x ↦ 1 / (x * log x ^ 2)) x

Tactic:
have : x * log x ^ 2 ≠ 0 := mul_ne_zero this <| by simp; grind

Goal state after:
x✝ x : ℝ
hx : x ∈ Set.Icc 2 x✝
this✝ : x ≠ 0
this : x * log x ^ 2 ≠ 0
⊢ ContinuousAt (fun x ↦ 1 / (x * log x ^ 2)) x
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
refine ⟨fun H ↦ ?_, zmodRepr_eq_zero_of_dvd⟩
  rw [← norm_lt_one_iff_dvd, ← sub_zero x, ← Nat.cast_zero, ← H]
  exact norm_sub_zmodRepr_lt_one _

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ Ideal.span {↑p}

Tactic:
rw [← maximalIdeal_eq_span_p]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑p} → x - ↑b ∈ Ideal.span {↑p} → ↑a = ↑b

Tactic:
rw [← maximalIdeal_eq_span_p]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ maximalIdeal ℤ_[p] → x - ↑b ∈ maximalIdeal ℤ_[p] → ↑a = ↑b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (∫ (x : ℝ) in 2..√x, 1 / log x ^ 2) + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
integral_1_div_log_sq_le two_le_sqrt (by linarith),

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg
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
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n) - ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val

Tactic:
simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]

Goal state after:
case neg
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
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n) - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs).cast
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A ⇑(b.reindex f) = discr A ⇑b

Tactic:
discr_def,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ (traceMatrix A ⇑(b.reindex f)).det = discr A ⇑b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inl
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
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast

Tactic:
simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]

Goal state after:
case neg.inl
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
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h)).cast
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (b ᵥ* P.map ⇑(algebraMap A B)) = P.det ^ 2 * discr A b

Tactic:
discr_def,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ (traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B))).det = P.det ^ 2 * discr A b
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ P.det * P.det * (traceMatrix A b).det = P.det ^ 2 * discr A b

Tactic:
discr_def,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ P.det * P.det * (traceMatrix A b).det = P.det ^ 2 * (traceMatrix A b).det
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ discr A (P.map ⇑(algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b

Tactic:
discr_def,

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ (traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b)).det = P.det ^ 2 * discr A b
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:
discr_def,

Goal state after:
ι : 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
⊢ (traceMatrix K ⇑b).det ≠ 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Tactic:
simp only [Ideal.mem_span_singleton]
  induction n with
  | zero => simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
  | succ n ih =>
    intro x
    dsimp only [appr]
    split_ifs with h
    · rw [h]
      apply dvd_zero
    push_cast
    rw [sub_add_eq_sub_sub]
    obtain ⟨c, hc⟩ := ih x
    simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]
    have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
    conv_rhs =>
      congr
      simp only [hc]
    rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
    rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
    apply mul_dvd_mul_left
    obtain hc0 | hc0 := eq_or_ne c.valuation 0
    · simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
      rw [mul_comm, unitCoeff_spec h] at hc
      suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
      lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
      rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
      exact irreducible_p
    · simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
      rw [unitCoeff_spec hc']
      exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
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
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2

Tactic:
discr_def,

Goal state after:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
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
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (traceMatrix K b).det = (embeddingsMatrixReindex K E b e).det ^ 2
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) i j)
⊢ discr ℚ ⇑b = discr ℚ ⇑b'

Tactic:
replace h' : ∀ i j, IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b')) i j) := by
    intro i j
    convert! h' i ((b.indexEquiv b').symm j)
    simp [Basis.toMatrix_apply]

Goal state after:
ι : 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)
⊢ discr ℚ ⇑b = discr ℚ ⇑b'
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝).comp (RingHom.id ℤ_[p]) = toZModPow n✝

Tactic:
RingHom.comp_id

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n✝ : ℕ
⊢ toZModPow n✝ = toZModPow n✝
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inr
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ (-1) ^ a = ((-1) ^ p ^ k) ^ a

pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ Odd (2 * (p ^ k * a) - 1)

Tactic:
hpo.pow.neg_one_pow

Goal state after:
case e_a.inr
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ (-1) ^ a = (-1) ^ a

p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2✝ : p = 2 → k ≠ 0
hp2 : p ≠ 2
hpo : Odd p
a : ℕ
ha : p - 1 = 2 * a
⊢ Odd (2 * (p ^ k * a) - 1)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ CommRing (ℤ√d)

Tactic:
refine
  { Zsqrtd.addGroupWithOne with
    npow := @npowRec (ℤ√d) ⟨1⟩ ⟨(· * ·)⟩,
    add_comm := ?_
    left_distrib := ?_
    right_distrib := ?_
    zero_mul := ?_
    mul_zero := ?_
    mul_assoc := ?_
    one_mul := ?_
    mul_one := ?_
    mul_comm := ?_ } <;>
  intros <;>
  ext

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im

case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im

case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).im = a✝.im

case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).re = a✝.re

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).im = a✝.im

case refine_5.re
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).re = re 0

case refine_5.im
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).im = im 0

case refine_6.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).re = re 0

case refine_6.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).im = im 0

case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im

case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im

case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).re = (b✝ * a✝).re

case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).im = (b✝ * a✝).im
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ ↑n ≤ pellZd a1 n

Tactic:
rw [Zsqrtd.natCast_val]

Goal state after:
a : ℕ
a1 : 1 < a
b : ℤ√↑(d a1)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ ↑n
⊢ { re := ↑n, im := 0 } ≤ pellZd a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
let t := pellZd_add a1 n (m - n)
  rw [add_tsub_cancel_of_le h] at t
  rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]

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

Goal state before:
pp: d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
i : ℕ
h : ↑y + -↑w = -↑i
⊢ -↑w + ↑y = -↑i

Tactic:
simp [add_comm, *]

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

Goal state before:
pp: d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : ↑x + -↑z = -↑i
⊢ -↑z + ↑x = -↑i

Tactic:
simp [add_comm, *]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
let t := xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] :=
  xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0

Tactic:
by
              simp only [Poly.map_apply] at ht
              rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
                funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl] at ht

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

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x ∈ s, f x = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := hxy

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList ~ m.primeFactorsList

Tactic:
filter_eq_self.mpr <| by grind

Goal state after:
case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ m.primeFactorsList ~ m.primeFactorsList
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: ⊢ smoothNumbers 0 = {1}

Tactic:
by
  simp only [smoothNumbers_eq_factoredNumbers, Finset.range_zero, factoredNumbers_empty]

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x ↦ ‖f x‖
⊢ Summable fun a ↦ ‖f p ^ a‖

Tactic:
simpa only [Function.comp_def, map_pow]
    using hsum.comp_injective <| Nat.pow_right_injective hp.one_lt

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

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

Tactic:
simp_rw [term_of_ne_zero hn, ← neg_div, ← neg_mul, mul_comm, mul_div_assoc, div_eq_mul_inv,
    ← cpow_neg]

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