mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ ((Algebra.leftMulMatrix b) 1).trace = 1

Tactic:
;

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ ((Algebra.leftMulMatrix b) 1).trace = 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
⊢ ofIntSeq 0 ⋯ = 0

Tactic:
;

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
⊢ ofIntSeq 0 ⋯ = 0
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a
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
⊢ traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = fun i ↦ (trace K L) (z * B.basis i)

Tactic:
;

Goal state after:
case e_a
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
⊢ traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = fun i ↦ (trace K L) (z * B.basis i)
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf ↑hζ.toRootsOfUnity]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x

Tactic:
← orderOf_units,

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
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf ↑↑hζ.toRootsOfUnity]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
⊢ lift f_compat = g

Tactic:
ext1 r
  apply eq_of_forall_dist_le
  intro ε hε
  obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
  apply le_trans _ (le_of_lt hn)
  rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker,
    map_sub, ← RingHom.comp_apply, ← RingHom.comp_apply, lift_spec, hg, sub_self]

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

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

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

Tactic:
;

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

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

Tactic:
simp only [_root_.pow_succ']

Goal state after:
case e_a.inl
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 * 2 ^ k * (2 * 2 ^ k - 1) / 2) = (-1) ^ (2 * 2 ^ k / 2)
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)
⊢ 0 < ↑p ^ n

Tactic:
;

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)
⊢ 0 < ↑p ^ n
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)
⊢ 0 < ↑p ^ n

Tactic:
exact_mod_cast Nat.pos_of_neZero _

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1

Tactic:
;

Goal state after:
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(a * a) - ↑1 = az a * az a - 1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(a * a) - ↑1 = az a * az a - 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(d a1 * y * y) = ↑1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell { re := ↑x, im := ↑y }
⊢ ↑(x * x) - ↑(d a1 * y * y) = ↑1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - d a1 * y * y = 1
⊢ ↑1 = 1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - d a1 * y * y = 1
⊢ ↑1 = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n) * ↑(xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
⊢ ↑(xn a1 n) * ↑(xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
h : ↑(xn a1 n * xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1
hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = ↑1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - ↑(d a1) * yz a1 n * yz a1 n = 1 := pell_eqz a1 n
h : ↑(xn a1 n * xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = 1
hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ ↑(xn a1 n * xn a1 n) - ↑(d a1 * yn a1 n * yn a1 n) = ↑1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ d a1 + 1 = a * a

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ d a1 + 1 = a * a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ a * a

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ a * a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this✝ : n * n + 1 = a * a
na : n < a
this : 1 + n * 2 + n ^ 2 ≤ 1 + n ^ 2
⊢ 1 + n * 2 + n ^ 2 ≤ 1 + n ^ 2

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this✝ : n * n + 1 = a * a
na : n < a
this : 1 + n * 2 + n ^ 2 ≤ 1 + n ^ 2
⊢ 1 + n * 2 + n ^ 2 ≤ 1 + n ^ 2
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_1.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_2.re
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).re = a✝.re

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_2.im
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).im = a✝.im

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).re = a✝.re

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).im = a✝.im

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).re = re 0

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).im = im 0

Tactic:
simp [add_comm, add_left_comm]

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

Goal state before:
pp: case refine_5.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

Tactic:
simp [add_comm, add_left_comm]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ { re := ↑a, im := 1 } * { re := ↑a, im := -1 } ≤ b * { re := ↑a, im := -1 }

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
⊢ { re := ↑a, im := 1 } * { re := ↑a, im := -1 } ≤ b * { re := ↑a, im := -1 }
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_5.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im

Tactic:
simp [add_comm, add_left_comm]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)

Tactic:
;

Goal state after:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = b * 1

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = b * 1
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ + x✝² + x✝¹) x✝ = (x✝³ + (x✝² + x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 + x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ + 0) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (-x✝¹ + x✝¹) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² + x✝¹) x✝ = (x✝¹ + x✝²) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * x✝² * x✝¹) x✝ = (x✝³ * (x✝² * x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (1 * x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 1) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 * x✝¹) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 0) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * (x✝² + x✝¹)) x✝ = (x✝³ * x✝² + x✝³ * x✝¹) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ x✝³ x✝ * (x✝² + x✝¹) x✝ = x✝³ x✝ * x✝² x✝ + x✝³ x✝ * x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ ((x✝³ + x✝²) * x✝¹) x✝ = (x✝³ * x✝¹ + x✝² * x✝¹) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ x✝ + x✝² x✝) * x✝¹ x✝ = x✝³ x✝ * x✝¹ x✝ + x✝² x✝ * x✝¹ x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y

Tactic:
ext <;> simp [sub_eq_add_neg, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
yl2 :
  { re := { re := x, im := y }.re + (-{ re := x, im := -y }).re,
      im := { re := x, im := y }.im + (-{ re := x, im := -y }).im } <
    { re := { re := ↑a, im := 1 }.re + (-{ re := ↑a, im := -1 }).re,
      im := { re := ↑a, im := 1 }.im + (-{ re := ↑a, im := -1 }).im }
y0l : 0 < { re := 0, im := y + y }
⊢ False

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
yl2 :
  { re := { re := x, im := y }.re + (-{ re := x, im := -y }).re,
      im := { re := x, im := y }.im + (-{ re := x, im := -y }).im } <
    { re := { re := ↑a, im := 1 }.re + (-{ re := ↑a, im := -1 }).re,
      im := { re := ↑a, im := 1 }.im + (-{ re := ↑a, im := -1 }).im }
y0l : 0 < { re := 0, im := y + y }
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - d a1 * y * y = 1
hp : 0 = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - d a1 * y * y = 1
hp : 0 = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
⊢ (∃ t, p (v ⊗ t) = 0) ↔ ∃ t, p ((v ⊗ t) ∘ (inl ⊗ inr ∘ f)) = 0
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
;

Goal state after:
case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (some b) = t b
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)

Tactic:
;

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d

Tactic:
;

Goal state after:
c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d