mathlib-initiative/mathlib-tactics huggingface dataset:
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 : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
use N

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
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 : R
n : ℕ
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
by
  obtain ⟨k, hk⟩ :=
    limNthHom_spec f_compat r _
      (show (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) from zpow_pos (mod_cast hp_prime.1.pos) _)
  have := le_of_lt (hk (max n k) (le_max_right _ _))
  rw [norm_le_pow_iff_mem_span_pow] at this
  dsimp [lift]
  rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]
  apply Ideal.add_mem _ _ this
  rw [Ideal.mem_span_singleton]
  convert!
    map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))
  · simp
  · simp [nthHom]

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

Goal state before:
pp: case e_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
H :
  derivative (cyclotomic (p ^ (k + 1)) K) * (X ^ p ^ k - 1) + cyclotomic (p ^ (k + 1)) K * derivative (X ^ p ^ k) =
    derivative (X ^ p ^ (k + 1) - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
derivative_X_pow,

Goal state after:
case e_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
H :
  derivative (cyclotomic (p ^ (k + 1)) K) * (X ^ p ^ k - 1) +
      cyclotomic (p ^ (k + 1)) K * (C ↑(p ^ k) * X ^ (p ^ k - 1)) =
    derivative (X ^ p ^ (k + 1) - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_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
H :
  derivative (cyclotomic (p ^ (k + 1)) K) * (X ^ p ^ k - 1) +
      cyclotomic (p ^ (k + 1)) K * (↑(p ^ k) * X ^ (p ^ k - 1)) =
    derivative (X ^ p ^ (k + 1))
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
derivative_X_pow,

Goal state after:
case e_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
H :
  derivative (cyclotomic (p ^ (k + 1)) K) * (X ^ p ^ k - 1) +
      cyclotomic (p ^ (k + 1)) K * (↑(p ^ k) * X ^ (p ^ k - 1)) =
    C ↑(p ^ (k + 1)) * X ^ (p ^ (k + 1) - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f + g)

Tactic:
rw [← sub_neg_eq_add]; exact hf.sub hg.neg

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

Goal state before:
pp: case refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = { re := ↑(a.re.gcd a.im) * re, im := ↑(a.re.gcd a.im) * im }

Tactic:
← Hre,

Goal state after:
case refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = { re := a.re, im := ↑(a.re.gcd a.im) * im }
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Goal state after:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑d * ↑w * ↑w - ↑z * ↑z)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) =
    (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Goal state after:
d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑z * ↑z - ↑d * ↑w * ↑w)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑(d * (x * w + y * z) * (x * w + y * z)) - ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Goal state after:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑d * ↑w * ↑w - ↑z * ↑z)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑(1 * (x * z + d * y * w) * (x * z + d * y * w)) - ↑(d * (x * w + y * z) * (x * w + y * z)) =
    (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))

Tactic:
simp only [one_mul, Int.natCast_add, Int.natCast_mul]

Goal state after:
d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑z * ↑z - ↑d * ↑w * ↑w)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case nil
α : Type u
d : List.Forall Dioph []
⊢ ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) [] ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl

Tactic:
| nil =>

Goal state after:
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
hζ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (0 + 1)) / 2) * ↑2 ^ (2 ^ (0 + 1 - 1) * ((2 - 1) * (0 + 1) - 1))

Tactic:
pow_one

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)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ✝).basis =
    (-1) ^ (φ (2 ^ (0 + 1)) / 2) * ↑2 ^ (2 ^ (0 + 1 - 1) * ((2 - 1) * (0 + 1) - 1))
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
⊢ IsCyclotomicExtension {p ^ 1} K L

Tactic:
pow_one

Goal state after:
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
⊢ IsCyclotomicExtension {p} K L
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Tactic:
let f : ℤ → ℤ := fun m => ⌊fract (ξ * m) * (n + 1)⌋
  have hn : 0 < (n : ℝ) + 1 := mod_cast Nat.succ_pos _
  have hfu := fun m : ℤ => mul_lt_of_lt_one_left hn <| fract_lt_one (ξ * ↑m)
  conv in |_| ≤ _ => rw [mul_comm, le_div_iff₀ hn, ← abs_of_pos hn, ← abs_mul]
  let D := Icc (0 : ℤ) n
  by_cases! H : ∃ m ∈ D, f m = n
  · obtain ⟨m, hm, hf⟩ := H
    have hf' : ((n : ℤ) : ℝ) ≤ fract (ξ * m) * (n + 1) := hf ▸ floor_le (fract (ξ * m) * (n + 1))
    have hm₀ : 0 < m := by
      have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
      refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
      exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)
    refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩
    rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]
    refine
      ⟨le_sub_iff_add_le.mpr ?_, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩
    simpa only [neg_add_cancel_comm_assoc] using! hf'
  · have hD : #(Ico (0 : ℤ) n) < #D := by rw [card_Icc, card_Ico]; exact lt_add_one n
    have hfu' : ∀ m, f m ≤ n := fun m => lt_add_one_iff.mp (floor_lt.mpr (mod_cast hfu m))
    have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico (0 : ℤ) n := fun x hx =>
      mem_Ico.mpr
        ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le), Ne.lt_of_le (H x hx) (hfu' x)⟩
    obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ : ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y := by
      obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
      rcases lt_trichotomy x y with (h | h | h)
      exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
    refine
      ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
        sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩
    convert_to! |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
    · congr; push_cast; simp only [fract]; ring
    exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

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
⊢ 1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])

Tactic:
rw [← hx, ← hy]
    refine ⟨a1,
        (Nat.eq_zero_or_pos k).elim (fun k0 => by rw [k0]; exact ⟨le_rfl, Or.inl ⟨rfl, rfl⟩⟩)
          fun kpos => ?_⟩
    exact
      let x := xn a1 k
      let y := yn a1 k
      let m := 2 * (k * y)
      let u := xn a1 m
      let v := yn a1 m
      have ky : k ≤ y := yn_ge_n a1 k
      have yv : y * y ∣ v := (ysq_dvd_yy a1 k).trans <| (y_dvd_iff _ _ _).2 <| dvd_mul_left _ _
      have uco : Nat.Coprime u (4 * y) :=
        have : 2 ∣ v :=
          modEq_zero_iff_dvd.1 <| (yn_modEq_two _ _).trans (dvd_mul_right _ _).modEq_zero_nat
        have : Nat.Coprime u 2 := (xy_coprime a1 m).coprime_dvd_right this
        (this.mul_right this).mul_right <|
          (xy_coprime _ _).coprime_dvd_right (dvd_of_mul_left_dvd yv)
      let ⟨b, ba, bm1⟩ := chineseRemainder uco a 1
      have m1 : 1 < m :=
        have : 0 < k * y := mul_pos kpos (strictMono_y a1 kpos)
        Nat.mul_le_mul_left 2 this
      have vp : 0 < v := strictMono_y a1 (lt_trans zero_lt_one m1)
      have b1 : 1 < b :=
        have : xn a1 1 < u := strictMono_x a1 m1
        have : a < u := by simpa using this
        lt_of_lt_of_le a1 <| by
          delta ModEq at ba; rw [Nat.mod_eq_of_lt this] at ba; rw [← ba]
          apply Nat.mod_le
      let s := xn b1 k
      let t := yn b1 k
      have sx : s ≡ x [MOD u] := (xy_modEq_of_modEq b1 a1 ba k).left
      have tk : t ≡ k [MOD 4 * y] :=
        have : 4 * y ∣ b - 1 :=
          Int.natCast_dvd_natCast.1 <| by rw [Int.ofNat_sub (le_of_lt b1)]; exact bm1.symm.dvd
        (yn_modEq_a_sub_one _ _).of_dvd this
      ⟨ky,
        Or.inr
          ⟨u, v, s, t, b, pell_eq _ _, pell_eq _ _, pell_eq _ _, b1, bm1, ba, vp, yv, sx, tk⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 0 = 1 ∧ yn a1 0 = 0

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
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
⊢ p ^ m.factorization p * ↑⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩ = m

Tactic:
← primeFactorsList_count_eq,

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
⊢ p ^ List.count p m.primeFactorsList * ↑⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩ = m
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1 ∣ ↑(yn a1 k) * ↑(xn hw1 j - n) + ↑(n ^ k) - ↑(xn a1 k)

Tactic:
Int.ofNat_sub na

Goal state after:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1 ∣ ↑(yn a1 k) * (↑(xn hw1 j) - ↑n) + ↑(n ^ k) - ↑(xn a1 k)
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < LSeries a ↑x

Tactic:
rw [LSeries]

Goal state after:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : abscissaOfAbsConv a < ↑x
⊢ 0 < ∑' (n : ℕ), term a (↑x) n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ),

Goal state after:
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ fract ξ ≤ 1⁻¹ ∧ (fract ξ)⁻¹ < 1 + 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
      (toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h

Goal state after:
case h.inr.inr
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(u - ⌊ξ⌋ * ↑v).toNat
⊢ ∃ n, ↑u / ↑v = ξ.convergent n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| ^ 1 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))

Tactic:
pow_one

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖ ≤ 2 * π * ↑|n| * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
step1 : HasSum (fun n ↦ jacobiTheta₂'_term n z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) ((jacobiTheta₂_fderiv z τ) (1, 0)) z
⊢ HasDerivAt (fun x ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z

Tactic:
← step1.tsum_eq

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
step2 : ∀ (n : ℤ), (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ
step1 : HasSum (fun n ↦ jacobiTheta₂'_term n z τ) ((jacobiTheta₂_fderiv z τ) (1, 0))
step3 : HasDerivAt (fun x ↦ jacobiTheta₂ x τ) (∑' (b : ℤ), jacobiTheta₂'_term b z τ) z
⊢ HasDerivAt (fun x ↦ jacobiTheta₂ x τ) (jacobiTheta₂' z τ) z
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ) *
      (cexp (-↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J) +
        (z * (cexp (-↑π * I * (τ + 2 * (z * τ))) * J) + cexp (-↑π * I * (τ + 2 * (z * τ))) * J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))

Tactic:
rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
    ← Complex.exp_add]

Goal state after:
z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))