Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
⊢ ↑cardPowDegree (x - z) < a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
⊢ ↑cardPowDegree (x - z) < a
have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ ↑cardPowDegree (x - z) < a

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
⊢ ↑cardPowDegree (x - z) < a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
⊢ ↑cardPowDegree (x - z) < a
by_cases hxy' : x = y
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ ↑cardPowDegree (x - z) < a

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
⊢ ↑cardPowDegree (x - z) < a
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
⊢ ↑cardPowDegree (x - z) < a
by_cases hyz' : y = z
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ ↑cardPowDegree (x - z) < a

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
⊢ ↑cardPowDegree (x - z) < a
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
⊢ ↑cardPowDegree (x - z) < a
by_cases hxz' : x = z
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) < a
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
⊢ ↑cardPowDegree (x - z) < a
rw [← Ne.def, ← sub_ne_zero] at hxy' hyz' hxz'
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) ≤ max (↑cardPowDegree (x - y)) (↑cardPowDegree (y - z))
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) < a
refine' lt_of_le_of_lt _ (max_lt hxy hyz)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) ≤ max (↑cardPowDegree (x - y)) (↑cardPowDegree (y - z))
rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy',
  cardPowDegree_nonzero _ hyz']
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
have : (1 : ℤ) ≤ Fintype.card Fq := by exact_mod_cast (@Fintype.one_lt_card Fq _ _).le
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (x - y) ∨
    ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (y - z)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
simp only [Int.cast_pow, Int.cast_ofNat, le_max_iff]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ natDegree (x - z) ≤ natDegree (x - y) ∨ natDegree (x - z) ≤ natDegree (y - z)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (x - y) ∨
    ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (y - z)
refine' Or.imp (pow_le_pow this) (pow_le_pow this) _
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ degree (x - z) ≤ max (degree (x - y)) (degree (y - z))
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ natDegree (x - z) ≤ natDegree (x - y) ∨ natDegree (x - z) ≤ natDegree (y - z)
rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ←
  degree_eq_natDegree hxy', ← degree_eq_natDegree hyz']
case h.e'_3.h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ x - z = x - y + (y - z)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ degree (x - z) ≤ max (degree (x - y)) (degree (y - z))
convert degree_add_le (x - y) (y - z) using 2
no goals
case h.e'_3.h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ x - z = x - y + (y - z)
exact (sub_add_sub_cancel _ _ _).symm
no goals
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ ↑cardPowDegree (x - z) < a
rwa [hxy']
no goals
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ ↑cardPowDegree (x - z) < a
rwa [← hyz']
no goals
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ ↑cardPowDegree (x - z) < a
rwa [hxz', sub_self, map_zero]
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ 1 ≤ ↑(Fintype.card Fq)
exact_mod_cast (@Fintype.one_lt_card Fq _ _).le