awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
neg : HPow.hPow (α := S) 1 deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp
⊢ p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
rw [← one_mul (p.coeff i), ← one_pow p.natDegree]

Premises used: one_pow, Polynomial.coeff, Polynomial.natDegree, one_mul
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ HPow.hPow (α := S) 1 deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
Submodule.mul_mem_mul (Submodule.pow_mem_pow Mq hq' _) (hp i)

Premises used: Submodule.mul_mem_mul, Set.Mem, Submodule.pow_mem_pow
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ HPow.hPow (α := S) 1 deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
exact Submodule.mul_mem_mul (Submodule.pow_mem_pow Mq hq' _) (hp i)

Premises used: Submodule.mul_mem_mul, Submodule.pow_mem_pow
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
pos : ∀ (H : q.Monic), (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp
neg : ∀ (H : ¬q.Monic), coeff 0 i ∈ Mq ^ deg(p) * Mp
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).1 else 0) i ∈ Mq ^ deg(p) * Mp

Tactic:
split_ifs with H
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).1

Premises used: SetLike.le_def, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
pos : HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
⊢ (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).1

Premises used: SetLike.le_def, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, And.left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ coeff 0 i ∈ Mq ^ deg(p) * Mp

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
rw :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
    (span (Set.range v))
rw₁ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v j /ₘ v i * v i))))
    (span (Set.range v))
rw₂ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (span (Set.range v))
rw₃ :
  Eq (α := Ideal R[X])
    (Submodule.span R[X] (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (span (Set.range v))
rw₄ :
  Eq (α := Ideal R[X])
    (Submodule.span R[X] (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (Submodule.span R[X] (Set.range v))
rw₅ rw₆ : Eq (α := Ideal R[X]) (Submodule.span R[X] (Set.range v)) (Submodule.span R[X] (Set.range v))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))

Tactic:
rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]

Premises used: Polynomial.modByMonic_eq_sub_mul_div, Submodule.span_range_update_sub_smul, mul_comm, Ideal.span, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
pos :
  ∀ (hp : p = 0),
    (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
neg :
  ∀ (hp : ¬p = 0),
    (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : p = 0
⊢ (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
pos :
  ∀ (hq : q = 0),
    (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
neg :
  ∀ (hq : ¬q = 0),
    (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p * q ≠ 0

Tactic:
have hpq : p * q ≠ 0 := mul_ne_zero hp hq
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p * q ≠ 0
⊢ (if p * q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p * q).natDegree) =
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) *
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp only [hpq, hp, hq, if_false, Polynomial.natDegree_mul hp hq, pow_add]

Premises used: Polynomial.natDegree_mul, if_false, pow_add
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
pos : p = 0 → LE.le (α := ℤ) 0 0
neg : ¬p = 0 → 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree
⊢ 0 ≤ if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : p = 0
⊢ LE.le (α := ℤ) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : ¬p = 0
⊢ 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree

Tactic:
pow_nonneg (Int.natCast_nonneg _) _

Premises used: pow_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : ¬p = 0
⊢ 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree

Tactic:
exact pow_nonneg (Int.natCast_nonneg _) _

Premises used: pow_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : ¬p = 0 → HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree = 0
contrapose! : ∀ (h : p ≠ 0), p ≠ 0 ∧ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree ≠ 0
⊢ p = 0

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree ≠ 0

Tactic:
⟨h, (pow_pos _).ne'⟩

Premises used: LT.lt.ne', And.intro
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree ≠ 0

Tactic:
exact ⟨h, (pow_pos _).ne'⟩
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
pos :
  ∀ (hp : p = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
neg :
  ∀ (hp : ¬p = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : p = 0
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
pos :
  ∀ (hq : q = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
neg :
  ∀ (hq : ¬q = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp [hq]
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
pos :
  ∀ (hpq : p + q = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
neg :
  ∀ (hpq : ¬p + q = 0),
    (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
      (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
        if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
by_cases hpq : p + q = 0
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
pos :
  0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp only [hpq, hp, hq, if_true, if_false]

Premises used: if_true, if_false
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
add_nonneg (pow_pos _).le (pow_pos _).le

Premises used: LT.lt.le, add_nonneg
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
exact add_nonneg (pow_pos _).le (pow_pos _).le

Premises used: LT.lt.le, add_nonneg
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
neg :
  HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree ≤
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
⊢ (if p + q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree) ≤
    (if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) +
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
simp only [hpq, hp, hq, if_false]

Premises used: if_false
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ (fun (x : ℕ) ↦ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) x) (max p.natDegree q.natDegree) ≤
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
grind
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree ≤
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree

Tactic:
exact le_trans (pow_right_mono₀ (by lia) (Polynomial.natDegree_add_le _ _)) (by grind)

Premises used: pow_right_mono₀, le_trans, Polynomial.natDegree_add_le
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
inst_2 : DecidableEq Fq
p : Fq[X]
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) p = if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree

Tactic:
simp [cardPowDegree]

Premises used: Polynomial.cardPowDegree
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
⊢ Eq (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) 0 : ℤ) (0 : ℤ)

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, Multiset.pmap, Multiset.attach, rfl, ite
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
p : Fq[X]
hp : p ≠ 0
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) p = HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree

Tactic:
if_neg hp

Premises used: if_neg, ite
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
simp :
  ((if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) <
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree) ↔
    p.degree < q.degree
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    p.degree < q.degree

Tactic:
simp only [cardPowDegree_apply]

Premises used: Polynomial.cardPowDegree_apply
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
pos : ∀ (hp : p = 0) (hq : q = 0), LT.lt (α := ℤ) 0 0 ↔ p.degree < q.degree
neg : ∀ (hp : p = 0) (hq : ¬q = 0), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree
pos₁ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
neg₁ :
  ∀ (hp : ¬p = 0) (hq : ¬q = 0),
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
      p.degree < q.degree
⊢ ((if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree) <
      if q = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree) ↔
    p.degree < q.degree

Tactic:
split_ifs with hp hq hq
-- Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree
Goal:
Fq : Type u_1
inst : Field Fq
inst_1 : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) n
p q : Fq[X]
hp : p = 0
hq : q = 0
⊢ LT.lt (α := ℤ) 0 0 ↔ p.degree < q.degree

Tactic:
simp only [hp, hq, lt_self_iff_false]

Premises used: lt_self_iff_false