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.traceMatrix ℤ (⇑b) default default = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)

Tactic:
Algebra.traceMatrix_apply,

Goal state after:
b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ ((Algebra.traceForm ℤ (𝓞 ℚ)) (b default)) (b default) = (Algebra.trace ℤ (𝓞 ℚ)) (b default * b default)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

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

Tactic:
by
      rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm,
        AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
        show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
        map_one, mul_one]

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

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

Goal state before:
pp: 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 s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ∀ j ≥ n, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
intro j

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 s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
⊢ j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
i : (_ : Fin pb.dim) × Fin pb.dim
x✝ : i ∈ univ.sigma fun i ↦ {i}ᶜ
⊢ (e i.snd) pb.gen - (e i.fst) pb.gen = ⟨e i.snd, (e i.fst) pb.gen⟩.fst pb.gen - ⟨e i.snd, (e i.fst) pb.gen⟩.snd

Tactic:
simp

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 k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ limNthHom f_compat r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]

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 : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑((f n) r).val + (limNthHom f_compat r - ↑(nthHom f r (max n k))) ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case e'_3
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 k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = (Int.castRingHom ℤ_[p]) (↑p ^ n)

Tactic:
simp

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

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

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

Goal state before:
pp: case zero
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ↑(p ^ k) ∣ f (k + 0) - f k

Tactic:
simp

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) < ε
i : ℕ
⊢ ↑(p ^ k) ∣ f (k + i) - f k

Tactic:
induction i with
  | zero => simp
  | succ n IH =>
    have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
    simpa using! (this.trans (hi _)).add IH

Goal state after:
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 - 1) * (2 ^ k.succ * (2 - 1) - 1) / 2) = (-1) ^ (2 ^ k.succ * (2 - 1) / 2)

Tactic:
rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]

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.zero
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)
inst✝ : IsCyclotomicExtension {2 ^ (succ 0 + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (succ 0 + 1))
hirr : Irreducible (cyclotomic (2 ^ (succ 0 + 1)) K)
hk : 2 ^ (succ 0 + 1) ≠ 2
hne : NeZero ↑(2 ^ (succ 0 + 1))
hp2 : 2 = 2 → succ 0 ≠ 0
⊢ (-1) ^ (2 ^ 0 * (2 * 2 ^ 0 - 1)) = (-1) ^ 2 ^ 0

Tactic:
simp

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))‖
⊢ 0 ≤ (↑p ^ n)⁻¹

Tactic:
simp

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

Goal state before:
pp: case zero
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
⊢ ↑(f (0 + n)) = ↑(f n)

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp

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:
rw [Pell.d, Int.ofNat_sub this]; rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simp

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 = b * 1

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re + b✝.re = b✝.re + a✝.re
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.im + b✝.im = b✝.im + a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.re + d * (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re + d * b✝.im * c✝.im) + d * a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re + d * b✝.im * c✝.im)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.re + c✝.re) + d * a✝.im * (b✝.im + c✝.im) =
    a✝.re * b✝.re + d * a✝.im * b✝.im + (a✝.re * c✝.re + d * a✝.im * c✝.im)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.re + d * (a✝.im + b✝.im) * c✝.im =
    a✝.re * c✝.re + d * a✝.im * c✝.im + (b✝.re * c✝.re + d * b✝.im * c✝.im)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.re + d * a✝.im * b✝.im = b✝.re * a✝.re + d * b✝.im * a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case re
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

Goal state after:
case im
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case re
d : ℤ
⊢ (sqrtd * sqrtd).re = (↑d).re

Tactic:
simp

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

Goal state before:
pp: case im
d : ℤ
⊢ (sqrtd * sqrtd).im = (↑d).im

Tactic:
simp

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

Goal state before:
pp: case re
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).re = { re := d * n * y, im := n * x }.re

Tactic:
simp

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

Goal state before:
pp: case im
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).im = { re := d * n * y, im := n * x }.im

Tactic:
simp

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

Goal state before:
pp: case re
d x y : ℤ
⊢ { re := x, im := y }.re = (↑x + sqrtd * ↑y).re

Tactic:
simp

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

Goal state before:
pp: case im
d x y : ℤ
⊢ { re := x, im := y }.im = (↑x + sqrtd * ↑y).im

Tactic:
simp

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

Goal state before:
pp: case mp
d z : ℤ
x : ℤ√d
⊢ z ∣ (↑z * x).re ∧ z ∣ (↑z * x).im

Tactic:
simp

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

Goal state before:
pp: d a b : ℤ
⊢ a ∣ (↑b).re ∧ a ∣ (↑b).im ↔ a ∣ b

Tactic:
simp

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✝ : ℤ
y0l : 0 < { re := 0, im := y✝ + y✝ }
yl2✝ : { re := 0, im := y✝ + y✝ } < { re := 0, im := 1 + 1 }
y : ℕ
x✝ : 0 < { re := 0, im := ↑(y + 1) + ↑(y + 1) }
yl2 : { re := 0, im := ↑(y + 1) + ↑(y + 1) } < { re := 0, im := 1 + 1 }
h1 : 1 ≤ { re := x, im := ↑(y + 1) }
hp : IsPell { re := x, im := ↑(y + 1) }
h : { re := x, im := ↑(y + 1) } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := ↑(y + 1) }
h1l : 1 < { re := x, im := ↑(y + 1) }
bm : { re := x, im := ↑(y + 1) } * { re := { re := x, im := ↑(y + 1) }.re, im := -{ re := x, im := ↑(y + 1) }.im } = 1
⊢ 0 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
n : ℤ
⊢ IsPoly fun v ↦ (const n) (v ∘ f)

Tactic:
by simpa using IsPoly.const _

Goal state after:
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
obtain ⟨t, ht⟩ := t

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

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

Tactic:
obtain ⟨t, ht⟩ := t

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

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

Tactic:
by
    have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
        fun e => by rw [e]
    simp only [xn_succ, gt_iff_lt]
    refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)
    have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
    rwa [mul_one] at t

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

Tactic:
rw [e]; apply y_mul_dvd

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case a
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]
⊢ yn a1 n ∣ d a1 * yn a1 (n * k)

Tactic:
apply dvd_mul_of_dvd_right

Goal state after:
case a
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]
⊢ yn a1 n ∣ yn a1 (n * k)
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
simp

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

Goal state before:
pp: d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := subNatNat x z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg

Tactic:
Int.subNatNat_eq_coe,

Goal state after:
d x y z w : ℕ
xy : { re := ↑x, im := -↑y }.Nonneg
zw : { re := -↑z, im := ↑w }.Nonneg
this : { re := ↑x - ↑z, im := subNatNat w y }.Nonneg
⊢ { re := ↑x + -↑z, im := ↑w - ↑y }.Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case zero
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
hζone : ζ = 1
⊢ Matrix.of (fun i j ↦ φ (p ^ 0) • 1) default default = 1 * ↑p ^ (p ^ (0 - 1) * (0 - 1))

Tactic:
simp

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
⊢ a.Nonneg ↔ (a - 0).Nonneg

Tactic:
simp

Goal state after:
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)
⊢ -1 = (algebraMap K L) (-1)

Tactic:
simp

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ ↑x + ↑d * ↑y.succ - ↑x = ↑d * ↑y.succ

Tactic:
simp

Goal state after:
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)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ -1 = (algebraMap K L) (-1)

Tactic:
simp

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

Goal state before:
pp: case pos.convert_2
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
⊢ φ (2 ^ (0 + 1)) • 1 = 1

Tactic:
simp

Goal state after: