awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
pos : HPow.hPow (α := K) 2 (HPow.hPow (α := ℕ) 2 (k₁ + 1)) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 (k₁ + 1))
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 k)

Tactic:
rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
      mul_pow, neg_one_sq, one_mul, ← pow_mul, ← _root_.pow_succ']

Premises used: neg_one_sq, pow_mul, IsPrimitiveRoot.norm_pow_sub_one_two, neg_eq_neg_one_mul, mul_pow, pow_succ', one_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ HPow.hPow (α := K) 2 (HPow.hPow (α := ℕ) 2 (k₁ + 1)) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 (k₁ + 1))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ¬p ^ (k - s + 1) = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ¬p ^ (k - s + 1) = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic n K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (zeta n K L) : K) (1 : K)

Tactic:
(zeta_spec n K L).norm_eq_one hn hirr

Premises used: IsPrimitiveRoot.norm_eq_one, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
n : ℕ
inst : NeZero n
K : Type u
L : Type v
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
hn : IsPrimePow n
inst_4 : IsCyclotomicExtension {n} K L
hirr : Irreducible (M := K[X]) (cyclotomic n K)
h : n ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (zeta n K L - 1) : K) ((↑n.minFac : K) : K)

Tactic:
(zeta_spec n K L).sub_one_norm_isPrimePow hn hirr h

Premises used: IsPrimitiveRoot.sub_one_norm_isPrimePow, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
k : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
⊢ (Algebra.norm K : (a : L) → K) (zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
(zeta_spec _ K L).norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
k : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
h : p ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (zeta (p ^ (k + 1)) K L - 1) : K) ((↑p : K) : K)

Tactic:
(zeta_spec _ K L).norm_sub_one_of_prime_ne_two hirr h

Premises used: IsPrimitiveRoot.norm_sub_one_of_prime_ne_two, IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Fact (Nat.Prime p)
inst_4 : IsCyclotomicExtension {p} K L
hirr : Irreducible (M := K[X]) (cyclotomic p K)
h : p ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (zeta p K L - 1) : K) ((↑p : K) : K)

Tactic:
(zeta_spec _ K L).norm_sub_one_of_prime_ne_two' hirr h

Premises used: IsPrimitiveRoot.norm_sub_one_of_prime_ne_two', IsCyclotomicExtension.zeta_spec
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
k : ℕ
hk : 2 ≤ k
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 k} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (zeta (HPow.hPow (α := ℕ) 2 k) K L - 1) : K) (2 : K)

Tactic:
norm_sub_one_two (zeta_spec (2 ^ k) K L) hk hirr

Premises used: HPow.hPow, IsCyclotomicExtension.zeta_spec, OfNat.ofNat, IsPrimitiveRoot.norm_sub_one_two
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f : (α → ℕ) → ℤ
rw : IsPoly f → IsPoly (0 - f)
⊢ IsPoly f → IsPoly (-f)

Tactic:
rw [← zero_sub]

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

Tactic:
(IsPoly.const 0).sub

Premises used: IsPoly.sub, OfNat.ofNat, IsPoly.const
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (0 - f)

Tactic:
exact (IsPoly.const 0).sub

Premises used: IsPoly.sub, OfNat.ofNat, IsPoly.const
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
rw : IsPoly (f - -g)
⊢ IsPoly (f + g)

Tactic:
rw [← sub_neg_eq_add]

Premises used: sub_neg_eq_add
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)

Tactic:
hf.sub hg.neg

Premises used: IsPoly.sub, IsPoly.neg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)

Tactic:
exact hf.sub hg.neg

Premises used: IsPoly.sub, IsPoly.neg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f : Poly α
⊢ IsPoly (α := α) (⇑f : (a : α → ℕ) → ℤ)

Tactic:
f.2

Premises used: Subtype.property
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
⊢ (∀ (x : α → ℕ), Eq (α := ℤ) ((f : (a : α → ℕ) → ℤ) x : ℤ) ((g : (a : α → ℕ) → ℤ) x : ℤ)) → f = g

Tactic:
DFunLike.ext _ _

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
i : α
x : α → ℕ
⊢ Eq (α := ℤ) ((proj i : (a : α → ℕ) → ℤ) x : ℤ) ((↑(x i) : ℤ) : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
n : ℤ
x : α → ℕ
⊢ (const n : (a : α → ℕ) → ℤ) x = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a : α → ℕ) → ℤ) (⇑0 : (a : α → ℕ) → ℤ) (⇑(const 0) : (a : α → ℕ) → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (a : α → ℕ) → ℤ) (⇑1 : (a : α → ℕ) → ℤ) (⇑(const 1) : (a : α → ℕ) → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f : Poly α
⊢ Eq (α := (a : α → ℕ) → ℤ) (⇑(-f) : (a : α → ℕ) → ℤ) (-(⇑f : (a : α → ℕ) → ℤ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
⊢ (⇑(f + g) : (a : α → ℕ) → ℤ) = HAdd.hAdd (α := (a : α → ℕ) → ℤ) (⇑f : (a : α → ℕ) → ℤ) (⇑g : (a : α → ℕ) → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
⊢ (⇑(f - g) : (a : α → ℕ) → ℤ) = HSub.hSub (α := (a : α → ℕ) → ℤ) (⇑f : (a : α → ℕ) → ℤ) (⇑g : (a : α → ℕ) → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
⊢ (⇑(f * g) : (a : α → ℕ) → ℤ) = HMul.hMul (α := (a : α → ℕ) → ℤ) (⇑f : (a : α → ℕ) → ℤ) (⇑g : (a : α → ℕ) → ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
x : α → ℕ
⊢ Eq (α := ℤ) ((0 : (a : α → ℕ) → ℤ) x : ℤ) (0 : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
x : α → ℕ
⊢ Eq (α := ℤ) ((1 : (a : α → ℕ) → ℤ) x : ℤ) (1 : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f : Poly α
x : α → ℕ
⊢ Eq (α := ℤ) ((-f : (a : α → ℕ) → ℤ) x : ℤ) (-(f : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: Int.neg, rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
x : α → ℕ
⊢ (f + g : (a : α → ℕ) → ℤ) x = HAdd.hAdd (α := ℤ) (β := ℤ) ((f : (a : α → ℕ) → ℤ) x : ℤ) ((g : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
x : α → ℕ
⊢ (f - g : (a : α → ℕ) → ℤ) x = HSub.hSub (α := ℤ) (β := ℤ) ((f : (a : α → ℕ) → ℤ) x : ℤ) ((g : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
f g : Poly α
x : α → ℕ
⊢ (f * g : (a : α → ℕ) → ℤ) x = HMul.hMul (α := ℤ) (β := ℤ) ((f : (a : α → ℕ) → ℤ) x : ℤ) ((g : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
a :
  ∀ (x_3 : α → ℕ), Eq (α := ℤ) ((x + x_1 + x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x + (x_1 + x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ)
⊢ x + x_1 + x_2 = x + (x_1 + x_2)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((0 + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ 0 + x = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HAdd.hAdd (α := ℤ) (β := ℤ) (0 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((0 + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
simp_rw [add_apply, zero_apply, zero_add]

Premises used: zero_add, Poly.add_apply, Poly.zero_apply
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x + 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ x + 0 = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (0 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((x + 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
simp_rw [add_apply, zero_apply, add_zero]

Premises used: Poly.add_apply, Poly.zero_apply, add_zero
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ -x + x = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((-x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ :
  HAdd.hAdd (α := ℤ) (β := ℤ) (-(x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₂ : Eq (α := ℤ) (0 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]

Premises used: Poly.neg_apply, Poly.add_apply, Poly.zero_apply, neg_add_cancel
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 : Poly α
a : ∀ (x_2 : α → ℕ), Eq (α := ℤ) ((x + x_1 : (a : α → ℕ) → ℤ) x_2 : ℤ) ((x_1 + x : (a : α → ℕ) → ℤ) x_2 : ℤ)
⊢ x + x_1 = x_1 + x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
a :
  ∀ (x_3 : α → ℕ), Eq (α := ℤ) ((x * x_1 * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * (x_1 * x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) (1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
a₂ a₃ : Eq (α := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ Eq (α := ℤ) ((1 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
rw [mul_apply, one_apply, one_mul]

Premises used: Poly.one_apply, Poly.mul_apply, one_mul
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ x * 1 = x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((1 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
a₂ a₃ : Eq (α := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ Eq (α := ℤ) ((x * 1 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
rw [mul_apply, one_apply, mul_one]

Premises used: Poly.one_apply, mul_one, Poly.mul_apply
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ 0 * x = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) (0 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = 0
a₂ a₃ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) ((0 * x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
rw [mul_apply, zero_apply, zero_mul]

Premises used: MulZeroClass.zero_mul, Poly.zero_apply, Poly.mul_apply
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
⊢ x * 0 = 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (0 : (a : α → ℕ) → ℤ) x_1
a₁ : HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (0 : ℤ) = 0
a₂ a₃ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) ((x * 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)

Tactic:
rw [mul_apply, zero_apply, mul_zero]

Premises used: MulZeroClass.mul_zero, Poly.zero_apply, Poly.mul_apply
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
a :
  ∀ (x_3 : α → ℕ),
    Eq (α := ℤ) ((x * (x_1 + x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * x_1 + x * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
x_3 : α → ℕ
⊢ HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_1 + x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_1 : (a : α → ℕ) → ℤ) x_3 : ℤ) +
      HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)

Tactic:
apply mul_add

Premises used: mul_add
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
a :
  ∀ (x_3 : α → ℕ),
    Eq (α := ℤ) (((x + x_1) * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x * x_2 + x_1 * x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
x_3 : α → ℕ
⊢ HMul.hMul (β := ℤ) (HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_1 : (a : α → ℕ) → ℤ) x_3 : ℤ))
      ((x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) +
      HMul.hMul (α := ℤ) (β := ℤ) ((x_1 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ)

Tactic:
apply add_mul

Premises used: add_mul
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
β : Type u_2
x x_1 : Poly α
a : ∀ (x_2 : α → ℕ), Eq (α := ℤ) ((x * x_1 : (a : α → ℕ) → ℤ) x_2 : ℤ) ((x_1 * x : (a : α → ℕ) → ℤ) x_2 : ℤ)
⊢ x * x_1 = x_1 * x

Tactic:
ext
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
obtain : ∀ (f : (α → ℕ) → ℤ) (pf : IsPoly f), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)
⊢ C f

Tactic:
obtain ⟨f, pf⟩ := f
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
i : α
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) ⋯)

Tactic:
apply H1
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
n : ℤ
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ n) ⋯)

Tactic:
apply H2
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f_1 g : (α → ℕ) → ℤ
h : IsPoly f_1
h_1 : IsPoly g
ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f_1 h)
ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g h_1)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f_1 x - g x) ⋯)

Tactic:
apply H3 _ _ ihf ihg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f_1 g : (α → ℕ) → ℤ
h : IsPoly f_1
h_1 : IsPoly g
ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f_1 h)
ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g h_1)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f_1 x * g x) ⋯)

Tactic:
apply H4 _ _ ihf ihg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (Poly.proj i)
H2 : ∀ (n : ℤ), C (Poly.const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
proj : ∀ (i : α), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ (↑(x i) : ℤ)) ⋯)
const : ∀ (n : ℤ), C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ n) ⋯)
sub :
  ∀ {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g)
    (ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f a))
    (ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g a_1)),
    C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f x - g x) ⋯)
mul :
  ∀ {f g : (α → ℕ) → ℤ} (a : IsPoly f) (a_1 : IsPoly g)
    (ihf : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f a))
    (ihg : C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) g a_1)),
    C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) (fun (x : α → ℕ) ↦ f x * g x) ⋯)
⊢ C (Subtype.mk (p := fun (f : (α → ℕ) → ℤ) ↦ IsPoly f) f pf)

Tactic:
induction pf with
  | proj => apply H1
  | const => apply H2
  | sub _ _ ihf ihg => apply H3 _ _ ihf ihg
  | mul _ _ ihf ihg => apply H4 _ _ ihf ihg

Premises used: Poly.proj, Poly.const
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ LE.le (α := ℤ) (0 : ℤ) ((p * p + sumsq ps : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)

Premises used: mul_self_nonneg, add_nonneg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ LE.le (α := ℤ) (0 : ℤ) ((p * p + sumsq ps : (a : α → ℕ) → ℤ) x : ℤ)

Tactic:
exact add_nonneg (mul_self_nonneg _) (sumsq_nonneg _ ps)

Premises used: add_nonneg
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ Eq (α := ℤ) ((sumsq (p :: ps) : (a : α → ℕ) → ℤ) x : ℤ) (0 : ℤ) ↔
    List.Forall (fun (a : Poly α) ↦ Eq (α := ℤ) ((a : (a : α → ℕ) → ℤ) x : ℤ) (0 : ℤ)) (p :: ps)

Tactic:
simp [sumsq, add_eq_zero_iff_of_nonneg, mul_self_nonneg, sumsq_eq_zero]

Premises used: mul_self_nonneg, add_eq_zero_iff_of_nonneg, Poly.sumsq
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
g : Poly α
i : α
⊢ (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f)) (proj i)

Tactic:
simpa using IsPoly.proj _

Premises used: IsPoly.proj
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
g : Poly α
n : ℤ
⊢ (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f)) (const n)

Tactic:
simpa using IsPoly.const _

Premises used: IsPoly.const
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
f_1 : α → β
g_1 f g : Poly α
pf : (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) f
pg : (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) g
⊢ (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) (f - g)

Tactic:
simpa using IsPoly.sub pf pg

Premises used: IsPoly.sub
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α_1 : Type u_1
β_1 : Type u_2
α : Type u_3
β : Type u_4
f_1 : α → β
g_1 f g : Poly α
pf : (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) f
pg : (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) g
⊢ (fun (g : Poly α) ↦ IsPoly.{u_4} (α := β) fun (v : β → ℕ) ↦ (g : (a : α → ℕ) → ℤ) (v ∘ f_1)) (f * g)

Tactic:
simpa using IsPoly.mul pf pg

Premises used: IsPoly.mul
-- Module: Mathlib.NumberTheory.Dioph
Goal:
α : Type u_3
β : Type u_4
f : α → β
g : Poly α
v : β → ℕ
⊢ Eq (α := ℤ) ((map f g : (a : β → ℕ) → ℤ) v : ℤ) ((g : (a : α → ℕ) → ℤ) (v ∘ f) : ℤ)

Tactic:
rfl

Premises used: rfl