[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
have hpq : p * q ≠ 0 := mul_ne_zero hp hq
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p * q ≠ 0
⊢ (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
      (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q
[PROOFSTEP]
simp only [hpq, hp, hq, eq_self_iff_true, if_true, if_false, Polynomial.natDegree_mul hp hq, pow_add]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
⊢ 0 ≤
    MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      p
[PROOFSTEP]
dsimp
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
⊢ 0 ≤ if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
split_ifs
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h✝ : p = 0
⊢ 0 ≤ 0
[PROOFSTEP]
rfl
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h✝ : ¬p = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
exact pow_nonneg (Int.ofNat_zero_le _) _
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h : ¬p = 0 → ↑(Fintype.card Fq) ^ natDegree p = 0
⊢ p = 0
[PROOFSTEP]
contrapose! h
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p : Fq[X]
h : p ≠ 0
⊢ p ≠ 0 ∧ ↑(Fintype.card Fq) ^ natDegree p ≠ 0
[PROOFSTEP]
exact ⟨h, (pow_pos _).ne'⟩
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp [hq]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
by_cases hpq : p + q = 0
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp only [hpq, hp, hq, eq_self_iff_true, if_true, if_false]
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
exact add_nonneg (pow_pos _).le (pow_pos _).le
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ MulHom.toFun
      { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
        map_mul' :=
          (_ :
            ∀ (p q : Fq[X]),
              (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
      (p + q) ≤
    MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        p +
      MulHom.toFun
        { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p,
          map_mul' :=
            (_ :
              ∀ (p q : Fq[X]),
                (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) (p * q) =
                  (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) p *
                    (fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) q) }
        q
[PROOFSTEP]
simp only [hpq, hp, hq, if_false]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree (p + q) ≤ ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
refine' le_trans (pow_le_pow (by linarith) (Polynomial.natDegree_add_le _ _)) _
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 1 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤
    ↑(Fintype.card Fq) ^ natDegree p + ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
refine' le_trans (le_max_iff.mpr _) (max_le_add_of_nonneg (pow_nonneg (by linarith) _) (pow_nonneg (by linarith) _))
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 0 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
linarith
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree p ∨
    ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
exact (max_choice p.natDegree q.natDegree).imp (fun h => by rw [h]) fun h => by rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
h : max (natDegree p) (natDegree q) = natDegree p
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree p
[PROOFSTEP]
rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
h : max (natDegree p) (natDegree q) = natDegree q
⊢ ↑(Fintype.card Fq) ^ max (natDegree p) (natDegree q) ≤ ↑(Fintype.card Fq) ^ natDegree q
[PROOFSTEP]
rw [h]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ↑cardPowDegree p < ↑cardPowDegree q ↔ EuclideanDomain.r p q
[PROOFSTEP]
show cardPowDegree p < cardPowDegree q ↔ degree p < degree q
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ↑cardPowDegree p < ↑cardPowDegree q ↔ degree p < degree q
[PROOFSTEP]
simp only [cardPowDegree_apply]
[GOAL]
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
⊢ ((if p = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree p) < if q = 0 then 0 else ↑(Fintype.card Fq) ^ natDegree q) ↔
    degree p < degree q
[PROOFSTEP]
split_ifs with hp hq hq
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : q = 0
⊢ 0 < 0 ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, lt_self_iff_false]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : p = 0
hq : ¬q = 0
⊢ 0 < ↑(Fintype.card Fq) ^ natDegree q ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, degree_zero, Ne.def, bot_lt_iff_ne_bot, degree_eq_bot, pow_pos, not_false_iff]
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree p < 0 ↔ degree p < degree q
[PROOFSTEP]
simp only [hp, hq, degree_zero, not_lt_bot, (pow_pos _).not_lt]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ ↑(Fintype.card Fq) ^ natDegree p < ↑(Fintype.card Fq) ^ natDegree q ↔ degree p < degree q
[PROOFSTEP]
rw [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe,
  pow_lt_pow_iff]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ 1 < ↑(Fintype.card Fq)
[PROOFSTEP]
exact_mod_cast @Fintype.one_lt_card Fq _ _
