awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw₅ : Eq (α := Ideal R[X]) (Submodule.span R[X] (Set.range v)) (Submodule.span R[X] (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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ (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
have 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
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ (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
have 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
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
have 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
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ (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
have 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
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (hypothesis)
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
have hpq : p * q ≠ 0
Tactic: have hpq : p * q ≠ 0 := mul_ne_zero hp hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ 0 ≤ if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree
have pos : p = 0 → LE.le (α := ℤ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ 0 ≤ if p = 0 then 0 else HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree
have neg : ¬p = 0 → 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ p = 0
have contrapose! : ∀ (h : p ≠ 0), p ≠ 0 ∧ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ (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
have 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
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ (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
have 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
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
have 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
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ (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
have 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
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
have 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
Tactic: by_cases hpq : p + q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ (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
have 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
Tactic: by_cases hpq : p + q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
have pos : 0 ≤ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
Tactic: simp only [hpq, hp, hq, if_true, if_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
have neg : HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (p + q).natDegree ≤
  HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree + HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree
Tactic: simp only [hpq, hp, hq, if_false]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    p.degree < q.degree
have 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
Tactic: simp only [cardPowDegree_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ ((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
have pos : ∀ (hp : p = 0) (hq : q = 0), LT.lt (α := ℤ) 0 0 ↔ p.degree < q.degree
Tactic: split_ifs with hp hq hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ ((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
have neg : ∀ (hp : p = 0) (hq : ¬q = 0), 0 < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔ p.degree < q.degree
Tactic: split_ifs with hp hq hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ ((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
have pos₁ : ∀ (hp : ¬p = 0) (hq : q = 0), HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < 0 ↔ p.degree < q.degree
Tactic: split_ifs with hp hq hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ ((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
have 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
Tactic: split_ifs with hp hq hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) p.natDegree < HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) q.natDegree ↔
    p.degree < q.degree
have neg : LT.lt (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
Tactic: rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q
have change : LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔ p.degree < q.degree
Tactic: classical
      change cardPowDegree p < cardPowDegree q ↔ degree p < degree q
      simp only [cardPowDegree_apply]
      split_ifs with hp hq hq
      · simp only [hp, hq, lt_self_iff_false]
      · simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]
      · simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]
      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
        exact mod_cast @Fintype.one_lt_card Fq _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
change :
  LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    p.degree < q.degree
⊢ LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    EuclideanDomain.r p q
have change₁ : ((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: classical
      change cardPowDegree p < cardPowDegree q ↔ degree p < degree q
      simp only [cardPowDegree_apply]
      split_ifs with hp hq hq
      · simp only [hp, hq, lt_self_iff_false]
      · simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]
      · simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]
      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
        exact mod_cast @Fintype.one_lt_card Fq _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.CardPowDegree (goal)
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]
change :
  LT.lt (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) p : ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) q : ℤ) ↔
    p.degree < q.degree
change₁ :
  ((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 : ℤ) ↔
    EuclideanDomain.r p q
have pos : ∀ (hp : p = 0) (hq : q = 0), LT.lt (α := ℤ) 0 0 ↔ p.degree < q.degree
Tactic: classical
      change cardPowDegree p < cardPowDegree q ↔ degree p < degree q
      simp only [cardPowDegree_apply]
      split_ifs with hp hq hq
      · simp only [hp, hq, lt_self_iff_false]
      · simp only [hp, hq, degree_zero, Ne, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos,
          not_false_iff]
      · simp only [hq, degree_zero, not_lt_bot, (pow_pos _).not_gt]
      · rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt, pow_lt_pow_iff_right₀]
        exact mod_cast @Fintype.one_lt_card Fq _ _