mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (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)

Tactic:
by

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

Goal state after:
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
n : ℕ
⊢ (toZModPow n).comp (lift f_compat) = f n

Tactic:
by

Goal state after:
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)ˣ
⊢ (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun
      ((fun t ↦ (IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯) x) =
    x

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen

Tactic:
by

Goal state after:
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)
⊢ (fromZetaAut hμ h) (zeta n K L) = μ

Tactic:
by

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

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

Goal state before:
pp: case refine_3
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ IsIntegral ℤ (subOnePowerBasis ℚ hζ).gen

pp: case refine_4
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)

Tactic:
· exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

Goal state after:
case refine_4
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
i : Fin (subOnePowerBasis ℚ hζ).dim
j : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim
⊢ minpoly ℚ (subOnePowerBasis ℚ hζ).gen = Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ (subOnePowerBasis ℚ hζ).gen)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = z

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
by

Goal state after:
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)
this : ∀ (i : Fin B.dim), ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) ↔ x = y

Tactic:
by

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

Goal state before:
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
⊢ p = 2 → k ≠ 0

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g') ↔ g = g'

Tactic:
by

Goal state after:
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
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
n : ℕ
IH : ↑(p ^ k) ∣ f (k + n) - f k
⊢ ↑p ^ (k + n) = ↑(p ^ k) * ↑p ^ n

Tactic:
by

Goal state after:
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
⊢ IsCauSeq (padicNorm p) fun x ↦ ↑(f x)

Tactic:
by

Goal state after:
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)
i : Fin B.dim
cramer :
  (1 *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    1 *ᵥ (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥

Tactic:
one_mulVec,

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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    1 *ᵥ (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ((traceMatrix K ⇑B.basis).det • B.basis.equivFun z) i ∈ ⊥
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:
by

Goal state after:
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)
H : ↑p ^ (-↑n) < ‖↑(↑(x.appr n) - f (N + n))‖
⊢ ‖↑p ^ n * ↑e‖ < ‖↑(↑(x.appr n) - f (N + n))‖

Tactic:
by

Goal state after:
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)
⊢ ‖↑(↑(x.appr n) - f (N + n))‖ ≤ ↑p ^ (-↑n)

Tactic:
by

Goal state after:
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 N : ℕ
IH : ↑(f (N + n)) = ↑(f n)
⊢ ↑p ^ (N + n) = ↑(p ^ n) * ↑p ^ N

Tactic:
by

Goal state after:
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 : ℕ
⊢ (toZModPow n) (ofIntSeq f ⋯) = ↑(f n)

Tactic:
by

Goal state after:
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
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e'_2
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ⇑b = ⇑b' ᵥ* (b'.toMatrix ⇑b).map ⇑(algebraMap ℤ A)

Tactic:
Basis.toMatrix_map_vecMul

Goal state after:
case e'_2
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ⇑b = ⇑b
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (b'.toMatrix ⇑b).det
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b = discr ℤ ⇑b'

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } * star { re := x, im := y } = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ { re := x, im := y } ∈ unitary (ℤ√d)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d : ℤ
b c : ℤ√d
hb : IsPell b
hc : IsPell c
⊢ b * c * star (b * c) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ IsPell { re := x, im := y } ↔ IsPell (star { re := x, im := y })

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ xn a1 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
⊢ yn a1 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by

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

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 1) = pellZd a1 n * { re := ↑a, im := 1 }

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ IsPell (pellZd a1 (n + 1))

Tactic:
by

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

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

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by

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

Tactic:
by

Goal state after:
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) ≤ n * n + 1

Tactic:
by

Goal state after:
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 : (n + 1) * (n + 1) ≤ n * n + 1
⊢ n + n + (n * n + 1) ≤ 0 + (n * n + 1)

Tactic:
by

Goal state after:
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✝ : (n + 1) * (n + 1) ≤ n * n + 1
this : n + n ≤ 0
⊢ d a1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ (n + 1) ≤ xn a1 (n + 1)

Tactic:
by

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

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

Tactic:
by

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
⊢ 1 ≤ b * { re := ↑a, im := -1 }

Tactic:
by

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

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

Tactic:
by

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
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 0 + x✝ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ + 0 = x✝

Tactic:
by

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
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = pellZd a1 (m + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ -x✝ + x✝ = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ x✝ : Poly α
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 1 * x✝ = x✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ * 1 = x✝

Tactic:
by

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

Goal state before:
pp: d : ℤ
a b : ℤ√d
⊢ star (a * b) = star b * star a

Tactic:
by

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

Goal state before:
pp: d : ℤ
⊢ ¬(re 0 = re 1 ∧ im 0 = im 1)

Tactic:
by

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

Goal state before:
pp: d n : ℤ
⊢ (↑n).re = n

Tactic:
by

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

Goal state before:
pp: d n : ℤ
⊢ (↑n).im = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 0 * x✝ = 0

Tactic:
by

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

Goal state before:
pp: d n : ℤ
⊢ ↑n = { re := n, im := 0 }

Tactic:
by

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

Goal state before:
pp: d : ℤ
m n : ℕ
⊢ ↑m = ↑n → m = n

Tactic:
by

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

Goal state before:
pp: d n : ℤ
⊢ ofInt n = ↑n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ * 0 = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: d a : ℤ
b : ℤ√d
⊢ (↑a * b).re = a * b.re

Tactic:
by

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

Goal state before:
pp: d a : ℤ
b : ℤ√d
⊢ (↑a * b).im = a * b.im

Tactic:
by

Goal state after:
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
hn : 1 ≤ { re := x, im := -y }
⊢ False

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: d : ℤ
⊢ sqrtd * sqrtd = ↑d

Tactic:
by

Goal state after: