mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case ofNat
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝) y = Nonnegg d c y (Int.ofNat a✝)

pp: case negSucc
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝) y = Nonnegg d c y (Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝) y = Nonnegg d c y (Int.ofNat a✝)

case negSucc
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝) y = Nonnegg d c y (Int.negSucc a✝)
Module: Mathlib.NumberTheory.Dioph

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case ofNat.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.ofNat a✝¹)

pp: case ofNat.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.ofNat a✝¹)

pp: case negSucc.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.negSucc a✝¹)

pp: case negSucc.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.negSucc a✝¹)

Tactic:
<;>

Goal state after:
case ofNat.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.ofNat a✝¹)

case ofNat.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.ofNat a✝¹)

case negSucc.ofNat
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.ofNat a✝) = Nonnegg d c (Int.ofNat a✝) (Int.negSucc a✝¹)

case negSucc.negSucc
c d a✝¹ a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝¹) (Int.negSucc a✝) = Nonnegg d c (Int.negSucc a✝) (Int.negSucc a✝¹)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case re
d : ℤ
n : ℤ√d
⊢ (↑n.norm).re = (n * star n).re

pp: case im
d : ℤ
n : ℤ√d
⊢ (↑n.norm).im = (n * star n).im

Tactic:
<;>

Goal state after:
case re
d : ℤ
n : ℤ√d
⊢ (↑n.norm).re = (n * star n).re

case im
d : ℤ
n : ℤ√d
⊢ (↑n.norm).im = (n * star n).im
Module: Mathlib.NumberTheory.PellMatiyasevic

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

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

Tactic:
<;>

Goal state after:
case zero
a : ℕ
a1 : 1 < a
n : ℕ
hx : xn a1 (n * 0) ≡ xn a1 n ^ 0 [MOD yn a1 n ^ 2]
hy : yn a1 (n * 0) ≡ 0 * xn a1 n ^ (0 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * 0) * xn a1 n + d a1 * yn a1 (n * 0) * yn a1 n ≡ xn a1 n ^ 0 * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ 0 * xn a1 n ^ (0 - 1) * yn a1 n * xn a1 n = 0 * xn a1 n ^ 0 * yn a1 n

case succ
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    yn a1 n ^ 2]
⊢ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n * xn a1 n = (k + 1) * xn a1 n ^ (k + 1) * yn a1 n
Module: Mathlib.NumberTheory.Dioph

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

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

Tactic:
<;>

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

case inr
α β : Type u
S : Set (α → ℕ)
f : α → β
γ : Type u
p : Poly (α ⊕ γ)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : β → ℕ
t : γ → ℕ
b : γ
⊢ (v ∘ f ⊗ t) (inr b) = ((v ⊗ t) ∘ (inl ∘ f ⊗ inr)) (inr b)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = re 0

pp: case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im = im 0

Tactic:
<;>

Goal state after:
case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = re 0

case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im = im 0
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.refine_1
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 (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ¬↑p ^ (k + 1) = 0
⊢ False

Tactic:
pow_eq_zero_iff (by lia)

Goal state after:
case e_a.refine_1
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 (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ¬↑p = 0
⊢ False
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inl
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
⊢ ({ re := ↑x, im := ↑y } + b).Nonneg

pp: case inr.inl
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + b).Nonneg

pp: case inr.inr
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + b).Nonneg

Tactic:
<;>

Goal state after:
case inl
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
⊢ ({ re := ↑x, im := ↑y } + b).Nonneg

case inr.inl
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + b).Nonneg

case inr.inr
d : ℕ
b : ℤ√↑d
hb : b.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + b).Nonneg
Module: Mathlib.NumberTheory.Dioph

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

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

Tactic:
<;>

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

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

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

pp: case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).im = (↑(2 * a) * pellZd a1 (n + 1)).im

Tactic:
<;>

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).re = (↑(2 * a) * pellZd a1 (n + 1)).re

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).im = (↑(2 * a) * pellZd a1 (n + 1)).im
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n)) * ↑a + (↑a * ↑a - 1) * (↑(xn a1 n) + ↑(yn a1 n) * ↑a) + ↑(xn a1 n) =
    2 * ↑a * (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n))

pp: case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n) + (↑(xn a1 n) + ↑(yn a1 n) * ↑a) * ↑a + ↑(yn a1 n) =
    2 * ↑a * (↑(xn a1 n) + ↑(yn a1 n) * ↑a)

Tactic:
<;>

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n)) * ↑a + (↑a * ↑a - 1) * (↑(xn a1 n) + ↑(yn a1 n) * ↑a) + ↑(xn a1 n) =
    2 * ↑a * (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n))

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n) + (↑(xn a1 n) + ↑(yn a1 n) * ↑a) * ↑a + ↑(yn a1 n) =
    2 * ↑a * (↑(xn a1 n) + ↑(yn a1 n) * ↑a)
Module: Mathlib.NumberTheory.Dioph

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

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

Tactic:
<;>

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

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

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

Tactic:
minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ (↑↑n * { re := -↑x, im := ↑y }).Nonneg

Tactic:
rw [smul_val]; simpa using! nonnegg_neg_pos.2 (sqLe_smul n <| nonnegg_neg_pos.1 ha)

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

Goal state before:
pp: case e'_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
i : Fin 1
⊢ ↑(e.symm i) = 0

Tactic:
← Nat.lt_one_iff

Goal state after:
case e'_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
i : Fin 1
⊢ ↑(e.symm i) < 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := -↑z, im := ↑w }).Nonneg

Tactic:
rw [calc
          (⟨x, -y⟩ * ⟨-z, w⟩ : ℤ√d) = ⟨_, _⟩ := rfl
          _ = ⟨-(x * z + d * y * w), x * w + y * z⟩ := by simp [add_comm]]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)

Tactic:
convert! discr_prime_pow_ne_two hζ' (by simpa [hirr]) (by simp [hodd]) using 2

Goal state after:
case e'_3.e'_5
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ (-1) ^ ((p - 1) / 2) = (-1) ^ (φ (p ^ (0 + 1)) / 2)

case e'_3.e'_6
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ ↑p ^ (p - 2) = ↑p ^ (p ^ 0 * ((p - 1) * (0 + 1) - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)

pp: case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)

Tactic:
<;>

Goal state after:
case inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)

case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl.inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ x) ⊗ t) (inl (inl val✝))

pp: case inl.inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ x) ⊗ t) (inl (inr val✝))

Tactic:
<;>

Goal state after:
case inl.inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ x) ⊗ t) (inl (inl val✝))

case inl.inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ x) ⊗ t) (inl (inr val✝))
Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions

Goal state before:
pp: ξ : ℝ
n : ℕ
⊢ (GenContFract.of ξ).convs n = ↑(ξ.convergent n)

Tactic:
induction n generalizing ξ with
  | zero => simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]
  | succ n ih => rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]; norm_cast

Goal state after: