mathlib-initiative/mathlib-tactics huggingface dataset:
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)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
hps,

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)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p ! =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)

Tactic:
have hb : b ≠ 0 := by
    rintro rfl
    specialize hA 0
    rw [degree_zero] at hA
    exact not_lt_of_ge bot_le hA
  -- Since there are > q^d elements of A, and only q^d choices for the highest `d` coefficients,
  -- there must be two elements of A with the same coefficients at
  -- `degree b - 1`, ... `degree b - d`.
  -- In other words, the following map is not injective:
  set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (natDegree b - j.succ)
  have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
    simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)
  -- Therefore, the differences have all coefficients higher than `deg b - d` equal.
  obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
  use i₀, i₁, i_ne
  refine (degree_lt_iff_coeff_zero _ _).mpr fun j hj => ?_
  -- The coefficients higher than `deg b` are the same because they are equal to 0.
  by_cases! hbj : degree b ≤ j
  · refine coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)
    exact lt_of_le_of_lt (degree_sub_le _ _) (max_lt (hA _) (hA _))
  -- So we only need to look for the coefficients between `deg b - d` and `deg b`.
  rw [coeff_sub, sub_eq_zero]
  rw [degree_eq_natDegree hb] at hbj
  have hbj : j < natDegree b := (@WithBot.coe_lt_coe _ _ _).mp hbj
  have hj : natDegree b - j.succ < d := by
    by_cases! hd : natDegree b < d
    · exact lt_of_le_of_lt tsub_le_self hd
    · have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
      rwa [tsub_lt_iff_tsub_lt hd hbj] at this
  have : j = b.natDegree - (natDegree b - j.succ).succ := by
    rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
  convert! congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ primorial n ∣ n.lcmUpto

Tactic:
simp only [primorial]

Goal state after:
n : ℕ
⊢ ∏ p ∈ range (n + 1) with Prime p, p ∣ n.lcmUpto
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n ≤ ↑(π n) * log ↑n

Tactic:
rw [psi_eq_sum_mul_log_prime, ← primesLE_card_eq_primeCounting, ← nsmul_eq_mul, ← sum_const]

Goal state after:
n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ (∑ x_1 ∈ Icc 1 N,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (x_1, y) with
            | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
          match (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0) =
    ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)

Tactic:
refine sum_congr rfl fun k _ ↦ ?_

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k : ℕ
x✝ : k ∈ Icc 1 N
⊢ (∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
      if
          match (k, y) with
          | (k, p) => p ≤ ⌊x ^ (↑k)⁻¹⌋₊ then
        match (k, y) with
        | (k, p) => f (p ^ k)
      else 0) =
    ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, f (p ^ k)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁✝ : Fin (n + 1)
i₁ : Fin n
⊢ t' i₁ = j ↔ ↑(cardPowDegree (A 0 % b - A i₁.succ % b)) < cardPowDegree b • ε

Tactic:
exact hj i₁

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ IntegrableOn (fun x ↦ 1 / (x * log x ^ 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) (Set.Icc 2 x) volume

Tactic:
refine integrableOn_mul_sum_Icc _ (by norm_num) <| ContinuousOn.integrableOn_Icc fun x hx ↦
    ContinuousAt.continuousWithinAt ?_

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

Goal state before:
pp: 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)

pp: 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)

Tactic:
· apply add_lt_add_of_lt_of_le (ih _)
        apply Nat.mul_le_mul_left
        apply le_pred_of_lt
        apply ZMod.val_lt

Goal state after:
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 : ℝ
hx : 1 < x
⊢ ↑(π ⌊x⌋₊) ≤ log 4 * x / log √x + √x

Tactic:
by
  have : 0 < log √x := log_pos (lt_sqrt_of_sq_lt (by simp [hx]))
  field_simp
  grind [pi_mul_log_sqrt_le hx.le]

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)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i)

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)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1

Tactic:
· exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

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)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ discr K ≠ 0

Tactic:
rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Algebra.discr ℚ ⇑(integralBasis K) ≠ ↑0
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
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r * s) j) - ↑(nthHom f r j) * ↑(nthHom f s j)) ≤ ↑p ^ (-↑n)

Tactic:
← Int.cast_mul,

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) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r * s) j) - ↑(nthHom f r j * nthHom f s j)) ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f : L ≃ₐ[K] L
⊢ ∀ ⦃a₂ : L ≃ₐ[K] L⦄, (autToPow K hμ) f = (autToPow K hμ) a₂ → f = a₂

Tactic:
g

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
⊢ (autToPow K hμ) f = (autToPow K hμ) g → f = g
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ B.basis i ∈ R[B.gen]

Tactic:
rw [B.basis_eq_pow i]

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ B.gen ^ ↑i ∈ R[B.gen]
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 : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ‖↑p ^ n * ↑e + ↑(↑(x.appr n) - f (N + n))‖ < ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)

Tactic:
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

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ‖↑p ^ n * ↑e + ↑(↑(x.appr n) - f (N + n))‖ < ↑p ^ (-↑n)
this : ‖↑(↑(x.appr n) - f (N + n))‖ ≤ ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
rw [_root_.pow_succ]

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

Goal state before:
pp: d : ℤ
x : ℤ√d
h : IsUnit x
⊢ x.norm.natAbs = 1

Tactic:
by
    let ⟨y, hy⟩ := isUnit_iff_dvd_one.1 h
    have := congr_arg (Int.natAbs ∘ norm) hy
    rw [Function.comp_apply, Function.comp_apply, norm_mul, Int.natAbs_mul, norm_one,
      Int.natAbs_one, eq_comm, mul_eq_one] at this
    exact this.1

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j

Tactic:
have h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j =
      (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j := by
    simp [add_mul, mul_assoc]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = (d a1 * yn a1 n * yn a1 n + 1) * xn a1 j
⊢ xn a1 n ∣ d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

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

Tactic:
hζ.eq_neg_one_of_two_right,

Goal state after:
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
⊢ (minpoly K (-1)).natDegree = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) - ↑(d a1) * yz a1 n * (xz a1 n * yz a1 j) + xz a1 j

Tactic:
sub_add_eq_add_sub

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(d a1) * yz a1 n * (xz a1 n * yz a1 j)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ ζ ^ ↑i) ∘ ⇑e.symm) = 1

Tactic:
hζ.eq_neg_one_of_two_right,

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ (-1) ^ ↑i) ∘ ⇑e.symm) = 1
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by rcases s with a | b <;> rfl

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
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
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ Irreducible (cyclotomic (p ^ (0 + 1)) ?m.146)

Tactic:
by simpa [hirr]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
s : Fin2 (n + 1)
⊢ ((x ::ₒ v) ∘ none :: some) s = (x :: v) s

Tactic:
by rcases s with a | b <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

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

Tactic:
← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,

Goal state after:
N k : ℕ
⊢ #({n ∈ Finset.range (N + 1) | n ∈ k.smoothNumbers} ∪ {n ∈ Finset.range (N + 1) | n ≠ 0 ∧ n ∉ k.smoothNumbers}) = N
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ m ^ 2 * s.prod id

Tactic:
← mul_one (m ^ 2)

Goal state after:
case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 * 1 ≤ m ^ 2 * s.prod id