[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∃ q, map f q = p
[PROOFSTEP]
simp only [coe_mapRingHom, lifts, RingHom.mem_rangeS]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ Set.range (map f)
[PROOFSTEP]
simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∀ (n : ℕ), coeff p n ∈ Set.range ↑f
[PROOFSTEP]
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) ↔ ∀ (n : ℕ), coeff p n ∈ Set.range ↑f
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
r : R
⊢ ↑(mapRingHom f) (↑C r) = ↑C (↑f r)
[PROOFSTEP]
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
s : S
h : s ∈ Set.range ↑f
⊢ ↑C s ∈ lifts f
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Set.mem_range.1 h
[GOAL]
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
r : R
h : ↑f r ∈ Set.range ↑f
⊢ ↑C (↑f r) ∈ lifts f
[PROOFSTEP]
use C r
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
r : R
h : ↑f r ∈ Set.range ↑f
⊢ ↑(mapRingHom f) (↑C r) = ↑C (↑f r)
[PROOFSTEP]
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
⊢ ↑(mapRingHom f) X = X
[PROOFSTEP]
simp only [coe_mapRingHom, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, map_X, and_self_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
⊢ ↑(mapRingHom f) (X ^ n) = X ^ n
[PROOFSTEP]
simp only [coe_mapRingHom, map_pow, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, map_X, and_self_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : p ∈ lifts f
⊢ ↑C (↑f r) * p ∈ lifts f
[PROOFSTEP]
simp only [lifts, RingHom.mem_rangeS] at hp ⊢
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
r : R
hp : ∃ x, ↑(mapRingHom f) x = p
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * p
[PROOFSTEP]
obtain ⟨p₁, rfl⟩ := hp
[GOAL]
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ∃ x, ↑(mapRingHom f) x = ↑C (↑f r) * ↑(mapRingHom f) p₁
[PROOFSTEP]
use C r * p₁
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
p₁ : R[X]
⊢ ↑(mapRingHom f) (↑C r * p₁) = ↑C (↑f r) * ↑(mapRingHom f) p₁
[PROOFSTEP]
simp only [coe_mapRingHom, map_C, map_mul]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
h : s ∈ Set.range ↑f
⊢ ↑(monomial n) s ∈ lifts f
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Set.mem_range.1 h
[GOAL]
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : ↑f r ∈ Set.range ↑f
⊢ ↑(monomial n) (↑f r) ∈ lifts f
[PROOFSTEP]
use monomial n r
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
r : R
h : ↑f r ∈ Set.range ↑f
⊢ ↑(mapRingHom f) (↑(monomial n) r) = ↑(monomial n) (↑f r)
[PROOFSTEP]
simp only [coe_mapRingHom, Set.mem_univ, map_monomial, Subsemiring.coe_top, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : p ∈ lifts f
⊢ erase n p ∈ lifts f
[PROOFSTEP]
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h ⊢
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (n_1 : ℕ), coeff (erase n p) n_1 ∈ RingHom.rangeS f
[PROOFSTEP]
intro k
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
[PROOFSTEP]
by_cases hk : k = n
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
[PROOFSTEP]
use 0
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : k = n
⊢ ↑f 0 = coeff (erase n p) k
[PROOFSTEP]
simp only [hk, RingHom.map_zero, erase_same]
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
[PROOFSTEP]
obtain ⟨i, hi⟩ := h k
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ coeff (erase n p) k ∈ RingHom.rangeS f
[PROOFSTEP]
use i
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
n : ℕ
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
k : ℕ
hk : ¬k = n
i : R
hi : ↑f i = coeff p k
⊢ ↑f i = coeff (erase n p) k
[PROOFSTEP]
simp only [hi, hk, erase_ne, Ne.def, not_false_iff]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : ↑(monomial n) s ∈ lifts f
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
by_cases hzero : s = 0
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : ↑(monomial n) s ∈ lifts f
hzero : s = 0
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
use 0
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : ↑(monomial n) s ∈ lifts f
hzero : s = 0
⊢ map f 0 = ↑(monomial n) s ∧ degree 0 = degree (↑(monomial n) s)
[PROOFSTEP]
simp only [hzero, degree_zero, eq_self_iff_true, and_self_iff, monomial_zero_right, Polynomial.map_zero]
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : ↑(monomial n) s ∈ lifts f
hzero : ¬s = 0
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
rw [lifts_iff_set_range] at hl
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hl : ↑(monomial n) s ∈ Set.range (map f)
hzero : ¬s = 0
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
obtain ⟨q, hq⟩ := hl
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : map f q = ↑(monomial n) s
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
replace hq := (ext_iff.1 hq) n
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
have hcoeff : f (q.coeff n) = s := by
  simp [coeff_monomial] at hq
  exact hq
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
⊢ ↑f (coeff q n) = s
[PROOFSTEP]
simp [coeff_monomial] at hq
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : ↑f (coeff q n) = s
⊢ ↑f (coeff q n) = s
[PROOFSTEP]
exact hq
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
⊢ ∃ q, map f q = ↑(monomial n) s ∧ degree q = degree (↑(monomial n) s)
[PROOFSTEP]
use monomial n (q.coeff n)
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
⊢ map f (↑(monomial n) (coeff q n)) = ↑(monomial n) s ∧ degree (↑(monomial n) (coeff q n)) = degree (↑(monomial n) s)
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
⊢ map f (↑(monomial n) (coeff q n)) = ↑(monomial n) s
[PROOFSTEP]
simp only [hcoeff, map_monomial]
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
⊢ degree (↑(monomial n) (coeff q n)) = degree (↑(monomial n) s)
[PROOFSTEP]
have hqzero : q.coeff n ≠ 0 := by
  intro habs
  simp only [habs, RingHom.map_zero] at hcoeff
  exact hzero hcoeff.symm
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
⊢ coeff q n ≠ 0
[PROOFSTEP]
intro habs
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
habs : coeff q n = 0
⊢ False
[PROOFSTEP]
simp only [habs, RingHom.map_zero] at hcoeff
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
habs : coeff q n = 0
hcoeff : 0 = s
⊢ False
[PROOFSTEP]
exact hzero hcoeff.symm
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
hqzero : coeff q n ≠ 0
⊢ degree (↑(monomial n) (coeff q n)) = degree (↑(monomial n) s)
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial]
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
hqzero : coeff q n ≠ 0
⊢ degree (↑C (coeff q n) * X ^ n) = degree (↑(monomial n) s)
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial]
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
n : ℕ
hzero : ¬s = 0
q : R[X]
hq : coeff (map f q) n = coeff (↑(monomial n) s) n
hcoeff : ↑f (coeff q n) = s
hqzero : coeff q n ≠ 0
⊢ degree (↑C (coeff q n) * X ^ n) = degree (↑C s * X ^ n)
[PROOFSTEP]
simp only [hzero, hqzero, Ne.def, not_false_iff, degree_C_mul_X_pow]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
generalize hd : p.natDegree = d
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
d : ℕ
hd : natDegree p = d
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
revert hd p
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
d : ℕ
⊢ ∀ {p : S[X]}, p ∈ lifts f → natDegree p = d → ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
induction' d using Nat.strong_induction_on with n hn
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
⊢ ∀ {p : S[X]}, p ∈ lifts f → natDegree p = n → ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
intros p hlifts hdeg
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
by_cases erase_zero : p.eraseLead = 0
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : eraseLead p = 0
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
rw [← eraseLead_add_monomial_natDegree_leadingCoeff p, erase_zero, zero_add, leadingCoeff]
[GOAL]
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : eraseLead p = 0
⊢ ∃ q,
    map f q = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
      degree q = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
[PROOFSTEP]
exact monomial_mem_lifts_and_degree_eq (monomial_mem_lifts p.natDegree ((lifts_iff_coeff_lifts p).1 hlifts p.natDegree))
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
have deg_erase := Or.resolve_right (eraseLead_natDegree_lt_or_eraseLead_eq_zero p) erase_zero
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
have pzero : p ≠ 0 := by
  intro habs
  exfalso
  rw [habs, eraseLead_zero, eq_self_iff_true, not_true] at erase_zero
  exact erase_zero
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
⊢ p ≠ 0
[PROOFSTEP]
intro habs
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
habs : p = 0
⊢ False
[PROOFSTEP]
exfalso
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
habs : p = 0
⊢ False
[PROOFSTEP]
rw [habs, eraseLead_zero, eq_self_iff_true, not_true] at erase_zero
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : False
deg_erase : natDegree (eraseLead p) < natDegree p
habs : p = 0
⊢ False
[PROOFSTEP]
exact erase_zero
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
have lead_zero : p.coeff p.natDegree ≠ 0 := by rw [← leadingCoeff, Ne.def, leadingCoeff_eq_zero]; exact pzero
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
⊢ coeff p (natDegree p) ≠ 0
[PROOFSTEP]
rw [← leadingCoeff, Ne.def, leadingCoeff_eq_zero]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
⊢ ¬p = 0
[PROOFSTEP]
exact pzero
[GOAL]
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
obtain ⟨lead, hlead⟩ :=
  monomial_mem_lifts_and_degree_eq (monomial_mem_lifts p.natDegree ((lifts_iff_coeff_lifts p).1 hlifts p.natDegree))
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
have deg_lead : lead.degree = p.natDegree := by
  rw [hlead.2, ← C_mul_X_pow_eq_monomial, degree_C_mul_X_pow p.natDegree lead_zero]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
⊢ degree lead = ↑(natDegree p)
[PROOFSTEP]
rw [hlead.2, ← C_mul_X_pow_eq_monomial, degree_C_mul_X_pow p.natDegree lead_zero]
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < natDegree p
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
rw [hdeg] at deg_erase
[GOAL]
case neg.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
obtain ⟨erase, herase⟩ :=
  hn p.eraseLead.natDegree deg_erase (erase_mem_lifts p.natDegree hlifts) (refl p.eraseLead.natDegree)
[GOAL]
case neg.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ ∃ q, map f q = p ∧ degree q = degree p
[PROOFSTEP]
use erase + lead
[GOAL]
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ map f (erase + lead) = p ∧ degree (erase + lead) = degree p
[PROOFSTEP]
constructor
[GOAL]
case h.left
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ map f (erase + lead) = p
[PROOFSTEP]
simp only [hlead, herase, Polynomial.map_add]
[GOAL]
case h.left
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ Polynomial.erase (natDegree p) p + ↑(monomial (natDegree p)) (coeff p (natDegree p)) = p
[PROOFSTEP]
rw [← eraseLead, ← leadingCoeff]
[GOAL]
case h.left
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ eraseLead p + ↑(monomial (natDegree p)) (leadingCoeff p) = p
[PROOFSTEP]
rw [eraseLead_add_monomial_natDegree_leadingCoeff p]
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ degree (erase + lead) = degree p
[PROOFSTEP]
rw [degree_eq_natDegree pzero, ← deg_lead]
[GOAL]
case h.right
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ degree (erase + lead) = degree lead
[PROOFSTEP]
apply degree_add_eq_right_of_degree_lt
[GOAL]
case h.right.h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ degree erase < degree lead
[PROOFSTEP]
rw [herase.2, deg_lead, ← degree_eq_natDegree pzero]
[GOAL]
case h.right.h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ {p : S[X]}, p ∈ lifts f → natDegree p = m → ∃ q, map f q = p ∧ degree q = degree p
p : S[X]
hlifts : p ∈ lifts f
hdeg : natDegree p = n
erase_zero : ¬eraseLead p = 0
deg_erase : natDegree (eraseLead p) < n
pzero : p ≠ 0
lead_zero : coeff p (natDegree p) ≠ 0
lead : R[X]
hlead :
  map f lead = ↑(monomial (natDegree p)) (coeff p (natDegree p)) ∧
    degree lead = degree (↑(monomial (natDegree p)) (coeff p (natDegree p)))
deg_lead : degree lead = ↑(natDegree p)
erase : R[X]
herase : map f erase = Polynomial.erase (natDegree p) p ∧ degree erase = degree (Polynomial.erase (natDegree p) p)
⊢ degree (Polynomial.erase (natDegree p) p) < degree p
[PROOFSTEP]
exact degree_erase_lt pzero
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
cases' subsingleton_or_nontrivial R with hR hR
[GOAL]
case inl
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Subsingleton R
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
obtain ⟨q, hq⟩ := mem_lifts_and_degree_eq hlifts
[GOAL]
case inl.intro
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Subsingleton R
q : R[X]
hq : map f q = p ∧ degree q = degree p
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
exact ⟨q, hq.1, hq.2, monic_of_subsingleton _⟩
[GOAL]
case inr
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
have H : erase p.natDegree p + X ^ p.natDegree = p := by
  simpa only [hp.leadingCoeff, C_1, one_mul, eraseLead] using eraseLead_add_C_mul_X_pow p
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
⊢ erase (natDegree p) p + X ^ natDegree p = p
[PROOFSTEP]
simpa only [hp.leadingCoeff, C_1, one_mul, eraseLead] using eraseLead_add_C_mul_X_pow p
[GOAL]
case inr
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
by_cases h0 : erase p.natDegree p = 0
[GOAL]
case pos
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : erase (natDegree p) p = 0
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
rw [← H, h0, zero_add]
[GOAL]
case pos
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : erase (natDegree p) p = 0
⊢ ∃ q, map f q = X ^ natDegree p ∧ degree q = degree (X ^ natDegree p) ∧ Monic q
[PROOFSTEP]
refine' ⟨X ^ p.natDegree, _, _, monic_X_pow p.natDegree⟩
[GOAL]
case pos.refine'_1
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : erase (natDegree p) p = 0
⊢ map f (X ^ natDegree p) = X ^ natDegree p
[PROOFSTEP]
rw [Polynomial.map_pow, map_X]
[GOAL]
case pos.refine'_2
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : erase (natDegree p) p = 0
⊢ degree (X ^ natDegree p) = degree (X ^ natDegree p)
[PROOFSTEP]
rw [degree_X_pow, degree_X_pow]
[GOAL]
case neg
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
obtain ⟨q, hq⟩ := mem_lifts_and_degree_eq (erase_mem_lifts p.natDegree hlifts)
[GOAL]
case neg.intro
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
have p_neq_0 : p ≠ 0 := by intro hp; apply h0; rw [hp]; simp only [natDegree_zero, erase_zero]
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
⊢ p ≠ 0
[PROOFSTEP]
intro hp
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp✝ : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
hp : p = 0
⊢ False
[PROOFSTEP]
apply h0
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp✝ : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
hp : p = 0
⊢ erase (natDegree p) p = 0
[PROOFSTEP]
rw [hp]
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp✝ : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
hp : p = 0
⊢ erase (natDegree 0) 0 = 0
[PROOFSTEP]
simp only [natDegree_zero, erase_zero]
[GOAL]
case neg.intro
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
have hdeg : q.degree < (X ^ p.natDegree).degree :=
  by
  rw [@degree_X_pow R, hq.2, ← degree_eq_natDegree p_neq_0]
  exact degree_erase_lt p_neq_0
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
⊢ degree q < degree (X ^ natDegree p)
[PROOFSTEP]
rw [@degree_X_pow R, hq.2, ← degree_eq_natDegree p_neq_0]
[GOAL]
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
⊢ degree (erase (natDegree p) p) < degree p
[PROOFSTEP]
exact degree_erase_lt p_neq_0
[GOAL]
case neg.intro
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
hdeg : degree q < degree (X ^ natDegree p)
⊢ ∃ q, map f q = p ∧ degree q = degree p ∧ Monic q
[PROOFSTEP]
refine' ⟨q + X ^ p.natDegree, _, _, (monic_X_pow _).add_of_right hdeg⟩
[GOAL]
case neg.intro.refine'_1
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
hdeg : degree q < degree (X ^ natDegree p)
⊢ map f (q + X ^ natDegree p) = p
[PROOFSTEP]
rw [Polynomial.map_add, hq.1, Polynomial.map_pow, map_X, H]
[GOAL]
case neg.intro.refine'_2
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial R
H : erase (natDegree p) p + X ^ natDegree p = p
h0 : ¬erase (natDegree p) p = 0
q : R[X]
hq : map f q = erase (natDegree p) p ∧ degree q = degree (erase (natDegree p) p)
p_neq_0 : p ≠ 0
hdeg : degree q < degree (X ^ natDegree p)
⊢ degree (q + X ^ natDegree p) = degree p
[PROOFSTEP]
rw [degree_add_eq_right_of_degree_lt hdeg, degree_X_pow, degree_eq_natDegree hp.ne_zero]
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
⊢ ∃ q, map f q = p ∧ natDegree q = natDegree p ∧ Monic q
[PROOFSTEP]
cases' subsingleton_or_nontrivial S with hR hR
[GOAL]
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Subsingleton S
⊢ ∃ q, map f q = p ∧ natDegree q = natDegree p ∧ Monic q
[PROOFSTEP]
obtain rfl : p = 1 := Subsingleton.elim _ _
[GOAL]
case inl
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ ∃ q, map f q = 1 ∧ natDegree q = natDegree 1 ∧ Monic q
[PROOFSTEP]
refine' ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ natDegree 1 = natDegree 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ Monic 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial S
⊢ ∃ q, map f q = p ∧ natDegree q = natDegree p ∧ Monic q
[PROOFSTEP]
obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
[GOAL]
case inr.intro.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
hlifts : p ∈ lifts f
hp : Monic p
hR : Nontrivial S
p' : R[X]
h₁ : map f p' = p
h₂ : degree p' = degree p
h₃ : Monic p'
⊢ ∃ q, map f q = p ∧ natDegree q = natDegree p ∧ Monic q
[PROOFSTEP]
exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩
[GOAL]
R : Type u
inst✝¹ : Ring R
S : Type v
inst✝ : Ring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ liftsRing f
[PROOFSTEP]
simp only [lifts, liftsRing, RingHom.mem_range, RingHom.mem_rangeS]
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ ↑(mapAlg R S) p = map (algebraMap R S) p
[PROOFSTEP]
simp only [mapAlg, aeval_def, eval₂_eq_sum, map, algebraMap_apply, RingHom.coe_comp]
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) = sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n✝ : ℕ
⊢ coeff (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) n✝ =
    coeff (sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e) n✝
[PROOFSTEP]
congr
[GOAL]
R✝ : Type u
inst✝⁵ : CommSemiring R✝
S✝ : Type v
inst✝⁴ : Semiring S✝
inst✝³ : Algebra R✝ S✝
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
⊢ p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (mapAlg R S)
[PROOFSTEP]
simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ lifts (algebraMap R S)
⊢ r • p ∈ lifts (algebraMap R S)
[PROOFSTEP]
rw [mem_lifts_iff_mem_alg] at hp ⊢
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : S[X]
r : R
hp : p ∈ AlgHom.range (mapAlg R S)
⊢ r • p ∈ AlgHom.range (mapAlg R S)
[PROOFSTEP]
exact Subalgebra.smul_mem (mapAlg R S).range hp r


[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ : β a₁ → WType fun a => β a
a₂ : α
f₂ : β a₂ → WType fun a => β a
h : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₂ f₂)
⊢ mk a₁ f₁ = mk a₂ f₂
[PROOFSTEP]
obtain ⟨rfl, h⟩ := Sigma.mk.inj_iff.mp (fγ_injective h)
[GOAL]
case intro
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
⊢ mk a₁ f₁ = mk a₁ f₂
[PROOFSTEP]
congr with x
[GOAL]
case intro.e_f.h
α : Type u_1
β : α → Type u_2
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
fγ_injective : Function.Injective fγ
a₁ : α
f₁ f₂ : β a₁ → WType fun a => β a
h✝ : elim γ fγ (mk a₁ f₁) = elim γ fγ (mk a₁ f₂)
h : HEq (fun b => elim γ fγ (f₁ b)) fun b => elim γ fγ (f₂ b)
x : β a₁
⊢ f₁ x = f₂ x
[PROOFSTEP]
exact elim_injective γ fγ fγ_injective (congr_fun (eq_of_heq h) x : _)
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
⊢ ¬Finite (WType β)
[PROOFSTEP]
intro hf
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
⊢ False
[PROOFSTEP]
have hba : b ≠ a := fun h => ha.elim (IsEmpty.elim' (show IsEmpty (β a) from h ▸ he))
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ False
[PROOFSTEP]
refine'
  not_injective_infinite_finite
    (fun n : ℕ => show WType β from Nat.recOn n ⟨b, IsEmpty.elim' he⟩ fun _ ih => ⟨a, fun _ => ih⟩) _
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
⊢ Function.Injective fun n =>
    let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
    this
[PROOFSTEP]
intro n m h
[GOAL]
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ n = m
[PROOFSTEP]
induction' n with n ih generalizing m
[GOAL]
case zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m✝ : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.zero = m
[PROOFSTEP]
cases' m with m
[GOAL]
case zero.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero
⊢ Nat.zero = Nat.zero
[PROOFSTEP]
simp_all
[GOAL]
case zero.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m✝ : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ Nat.zero = Nat.succ m
[PROOFSTEP]
simp_all
[GOAL]
case succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n✝ m✝ : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
⊢ Nat.succ n = m
[PROOFSTEP]
cases' m with m
[GOAL]
case succ.zero
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n✝ m : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      Nat.zero
⊢ Nat.succ n = Nat.zero
[PROOFSTEP]
simp_all
[GOAL]
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n✝ m✝ : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ Nat.succ n = Nat.succ m
[PROOFSTEP]
refine' congr_arg Nat.succ (ih _)
[GOAL]
case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n✝ m✝ : ℕ
h✝ :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n✝ =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m✝
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          n =
        (fun n =>
            let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ n) =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      (Nat.succ m)
⊢ (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      n =
    (fun n =>
        let_fun this := Nat.recOn n (mk b (IsEmpty.elim' he)) fun x ih => mk a fun x => ih;
        this)
      m
[PROOFSTEP]
simp_all [Function.funext_iff]
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < depth t
[PROOFSTEP]
cases t
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < depth (mk a✝ f✝)
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType.WType' β 0 → Empty :=
  fun x =>
    match x with
    | { val := x, property := h } => False.elim (_ : False)
⊢ Empty → WType.WType' β 0
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
f : WType.WType' β 0 → Empty :=
  fun x =>
    match x with
    | { val := x, property := h } => False.elim (_ : False)
x : Empty
⊢ WType.WType' β 0
[PROOFSTEP]
cases x
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
t : WType β
h : depth t ≤ n + 1
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
cases' t with a f
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : depth (mk a f) ≤ n + 1
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
have h₀ : ∀ i : β a, WType.depth (f i) ≤ n := fun i =>
  Nat.le_of_lt_succ (lt_of_lt_of_le (WType.depth_lt_depth_mk a f i) h)
[GOAL]
case mk
α : Type u_1
β : α → Type u_2
inst✝¹ : (a : α) → Fintype (β a)
inst✝ : (a : α) → Encodable (β a)
n : ℕ
a : α
f : β a → WType β
h : depth (mk a f) ≤ n + 1
h₀ : ∀ (i : β a), depth (f i) ≤ n
⊢ (a : α) × (β a → WType.WType' β n)
[PROOFSTEP]
exact ⟨a, fun i : β a => ⟨f i, h₀ i⟩⟩
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
h : Encodable (WType.WType' β n)
⊢ ∀ (b : WType.WType' β (n + 1)), WType.finv n (WType.f n b) = b
[PROOFSTEP]
rintro ⟨⟨_, _⟩, _⟩
[GOAL]
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
n : ℕ
h : Encodable (WType.WType' β n)
a✝ : α
f✝ : β a✝ → WType β
property✝ : depth (mk a✝ f✝) ≤ n + 1
⊢ WType.finv n (WType.f n { val := mk a✝ f✝, property := property✝ }) = { val := mk a✝ f✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
⊢ Encodable (WType β)
[PROOFSTEP]
haveI h' : ∀ n, Encodable (WType' β n) := fun n => Nat.rec encodable_zero encodable_succ n
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
⊢ Encodable (WType β)
[PROOFSTEP]
let f : WType β → Σ n, WType' β n := fun t => ⟨t.depth, ⟨t, le_rfl⟩⟩
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
⊢ Encodable (WType β)
[PROOFSTEP]
let finv : (Σ n, WType' β n) → WType β := fun p => p.2.1
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
finv : (n : ℕ) × WType.WType' β n → WType β := fun p => ↑p.snd
⊢ Encodable (WType β)
[PROOFSTEP]
have : ∀ t, finv (f t) = t := fun t => rfl
[GOAL]
α : Type u_1
β : α → Type u_2
inst✝² : (a : α) → Fintype (β a)
inst✝¹ : (a : α) → Encodable (β a)
inst✝ : Encodable α
h' : (n : ℕ) → Encodable (WType.WType' β n)
f : WType β → (n : ℕ) × WType.WType' β n :=
  fun t => { fst := depth t, snd := { val := t, property := (_ : depth t ≤ depth t) } }
finv : (n : ℕ) × WType.WType' β n → WType β := fun p => ↑p.snd
this : ∀ (t : WType β), finv (f t) = t
⊢ Encodable (WType β)
[PROOFSTEP]
exact Encodable.ofLeftInverse f finv this


[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α ⊕ β)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α ⊕ β)
[PROOFSTEP]
rcases exists_injective_nat β with ⟨g, hg⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α ⊕ β)
[PROOFSTEP]
exact (Equiv.natSumNatEquivNat.injective.comp <| hf.sum_map hg).countable
[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
⊢ Countable (α × β)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
⊢ Countable (α × β)
[PROOFSTEP]
rcases exists_injective_nat β with ⟨g, hg⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : Countable β
f : α → ℕ
hf : Injective f
g : β → ℕ
hg : Injective g
⊢ Countable (α × β)
[PROOFSTEP]
exact (Nat.pairEquiv.injective.comp <| hf.Prod_map hg).countable
[GOAL]
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Sigma π)
[PROOFSTEP]
rcases exists_injective_nat α with ⟨f, hf⟩
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
⊢ Countable (Sigma π)
[PROOFSTEP]
choose g hg using fun a => exists_injective_nat (π a)
[GOAL]
case intro
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Countable α
inst✝ : ∀ (a : α), Countable (π a)
f : α → ℕ
hf : Injective f
g : (a : α) → π a → ℕ
hg : ∀ (a : α), Injective (g a)
⊢ Countable (Sigma π)
[PROOFSTEP]
exact ((Equiv.sigmaEquivProd ℕ ℕ).injective.comp <| hf.sigma_map hg).countable
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
have : ∀ n, Countable (Fin n → ℕ) := by
  intro n
  induction' n with n ihn
  · change Countable (Fin 0 → ℕ); infer_instance
  · haveI := ihn
    exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Equiv.piFinSucc _ _).symm
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ ∀ (n : ℕ), Countable (Fin n → ℕ)
[PROOFSTEP]
intro n
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
⊢ Countable (Fin n → ℕ)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin Nat.zero → ℕ)
[PROOFSTEP]
change Countable (Fin 0 → ℕ)
[GOAL]
case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin 0 → ℕ)
[PROOFSTEP]
infer_instance
[GOAL]
case succ
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
ihn : Countable (Fin n → ℕ)
⊢ Countable (Fin (Nat.succ n) → ℕ)
[PROOFSTEP]
haveI := ihn
[GOAL]
case succ
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
n : ℕ
ihn this : Countable (Fin n → ℕ)
⊢ Countable (Fin (Nat.succ n) → ℕ)
[PROOFSTEP]
exact Countable.of_equiv (ℕ × (Fin n → ℕ)) (Equiv.piFinSucc _ _).symm
[GOAL]
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
[GOAL]
case intro.intro
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
have f := fun a => (nonempty_embedding_nat (π a)).some
[GOAL]
case intro.intro
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → π a ↪ ℕ
⊢ Countable ((a : α) → π a)
[PROOFSTEP]
exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable


[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p = 0
⊢ trailingDegree p = ⊤
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt trailingDegree_eq_top.1 hp))
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ trailingDegree p
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
have hn : trailingDegree p = n := Classical.not_not.1 hn
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ trailingDegree p = ↑(natTrailingDegree p)
[PROOFSTEP]
rw [natTrailingDegree, hn]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ ↑n = ↑(Option.getD (↑n) 0)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hp : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
exact WithTop.coe_eq_coe
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n → natTrailingDegree p = n
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
[PROOFSTEP]
rwa [← trailingDegree_eq_iff_natTrailingDegree_eq]
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree 0 = ↑n
⊢ False
[PROOFSTEP]
rw [trailingDegree_zero] at H
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : ⊤ = ↑n
⊢ False
[PROOFSTEP]
exact Option.noConfusion H
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ natTrailingDegree p = n → trailingDegree p = ↑n
[PROOFSTEP]
intro H
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ trailingDegree p = ↑n
[PROOFSTEP]
rwa [trailingDegree_eq_iff_natTrailingDegree_eq]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree 0 = n
⊢ False
[PROOFSTEP]
rw [natTrailingDegree_zero] at H
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : 0 = n
⊢ False
[PROOFSTEP]
rw [H] at hn
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n < n
H : 0 = n
⊢ False
[PROOFSTEP]
exact lt_irrefl _ hn
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p = 0
⊢ False
[PROOFSTEP]
rw [hp0] at h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree 0 = ↑n
hp0 : p = 0
⊢ False
[PROOFSTEP]
exact Option.noConfusion h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : trailingDegree p = ↑n
hp0 : p ≠ 0
⊢ ↑(natTrailingDegree p) = ↑n
[PROOFSTEP]
rwa [← trailingDegree_eq_natTrailingDegree hp0]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
rw [hp, trailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p = 0
⊢ ↑(natTrailingDegree 0) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : ¬p = 0
⊢ ↑(natTrailingDegree p) ≤ trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ natTrailingDegree p = natTrailingDegree q
[PROOFSTEP]
unfold natTrailingDegree
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ Option.getD (trailingDegree p) 0 = Option.getD (trailingDegree q) 0
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
have : WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p ≤ n
[PROOFSTEP]
rw [← WithTop.coe_le_coe, this, ← trailingDegree_eq_natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p ≤ ↑n
[PROOFSTEP]
exact le_trailingDegree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ p ≠ 0
[PROOFSTEP]
intro h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h✝ : coeff p n ≠ 0
this : ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
h : p = 0
⊢ False
[PROOFSTEP]
subst h
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
q r : R[X]
h : coeff 0 n ≠ 0
this : ↑(natTrailingDegree 0) = ↑(natTrailingDegree 0)
⊢ False
[PROOFSTEP]
exact h rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : p = 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
rw [hp]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : p = 0
⊢ trailingDegree q ≤ trailingDegree 0
[PROOFSTEP]
exact le_top
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : ¬p = 0
⊢ trailingDegree q ≤ trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : coeff q (natTrailingDegree p) ≠ 0
hp : ¬p = 0
⊢ trailingDegree q ≤ ↑(natTrailingDegree p)
[PROOFSTEP]
exact le_trailingDegree_of_ne_zero h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
[PROOFSTEP]
have : Nat.cast n = WithTop.some n := rfl
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
[PROOFSTEP]
exact mt fun h => by rw [natTrailingDegree, h, this, ← WithTop.some_eq_coe, Option.getD_some]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
h : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
[PROOFSTEP]
rw [natTrailingDegree, h, this, ← WithTop.some_eq_coe, Option.getD_some]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ trailingDegree p
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp] at H
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ ↑(natTrailingDegree p)
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
exact WithTop.coe_le_coe.mp H
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
rw [hp, natTrailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : p = 0
⊢ 0 ≤ natTrailingDegree q
[PROOFSTEP]
exact zero_le _
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : trailingDegree p ≤ trailingDegree q
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq] at hpq
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hq : q ≠ 0
hpq : ↑(natTrailingDegree p) ≤ ↑(natTrailingDegree q)
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natTrailingDegree q
[PROOFSTEP]
exact WithTop.coe_le_coe.1 hpq
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ trailingDegree (↑(monomial n) a) = ↑n
[PROOFSTEP]
rw [trailingDegree, support_monomial n ha, min_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ natTrailingDegree (↑(monomial n) a) = n
[PROOFSTEP]
rw [natTrailingDegree, trailingDegree_monomial ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a ≠ 0
⊢ Option.getD (↑n) 0 = n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a = 0
⊢ natTrailingDegree (↑(monomial n) a) ≤ n
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
ha : a = 0
⊢ ↑n ≤ trailingDegree (↑(monomial n) a)
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ 0 ≤ trailingDegree 1
[PROOFSTEP]
rw [← C_1]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ 0 ≤ trailingDegree (↑C 1)
[PROOFSTEP]
exact le_trailingDegree_C
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natTrailingDegree ↑n = 0
[PROOFSTEP]
simp only [← C_eq_nat_cast, natTrailingDegree_C]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
ha : a ≠ 0
⊢ trailingDegree (↑C a * X ^ n) = ↑n
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ ↑n ≤ trailingDegree (↑C a * X ^ n)
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ ↑n ≤ trailingDegree (↑(monomial n) a)
[PROOFSTEP]
exact le_trailingDegree_monomial
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ coeff p n = 0
[PROOFSTEP]
apply coeff_eq_zero_of_trailingDegree_lt
[GOAL]
case h
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
⊢ ↑n < trailingDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < trailingDegree p
[PROOFSTEP]
rw [hp, trailingDegree_zero]
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : p = 0
⊢ ↑n < ⊤
[PROOFSTEP]
exact WithTop.coe_lt_top n
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < trailingDegree p
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
h : n < natTrailingDegree p
hp : ¬p = 0
⊢ ↑n < ↑(natTrailingDegree p)
[PROOFSTEP]
exact WithTop.coe_lt_coe.2 h
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ ↑n ≤ trailingDegree (X ^ n)
[PROOFSTEP]
simpa only [C_1, one_mul] using le_trailingDegree_C_mul_X_pow n (1 : R)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p = min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p ≤ min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
apply le_min'
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ ∀ (y : ℕ), y ∈ support p → natTrailingDegree p ≤ y
[PROOFSTEP]
intro y hy
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
y : ℕ
hy : y ∈ support p
⊢ natTrailingDegree p ≤ y
[PROOFSTEP]
exact natTrailingDegree_le_of_mem_supp y hy
[GOAL]
case a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ min' (support p) (_ : Finset.Nonempty (support p)) ≤ natTrailingDegree p
[PROOFSTEP]
apply Finset.min'_le
[GOAL]
case a.H2
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p ≠ 0
⊢ natTrailingDegree p ∈ support p
[PROOFSTEP]
exact mem_support_iff.mpr (trailingCoeff_nonzero_iff_nonzero.mpr h)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hn : ∀ (m : ℕ), m < n → coeff p m = 0
⊢ n ≤ natTrailingDegree p
[PROOFSTEP]
rw [natTrailingDegree_eq_support_min' hp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
hn : ∀ (m : ℕ), m < n → coeff p m = 0
⊢ n ≤ min' (support p) (_ : Finset.Nonempty (support p))
[PROOFSTEP]
exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p = 0
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
rw [hp, natDegree_zero, natTrailingDegree_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : ¬p = 0
⊢ natTrailingDegree p ≤ natDegree p
[PROOFSTEP]
exact le_natDegree_of_ne_zero (mt trailingCoeff_eq_zero.mp hp)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree (p * X ^ n) = natTrailingDegree p + n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree (p * X ^ n) ≤ natTrailingDegree p + n
[PROOFSTEP]
refine' natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp _
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
h : coeff (p * X ^ n) (natTrailingDegree p + n) = 0
⊢ trailingCoeff p = 0
[PROOFSTEP]
rwa [trailingCoeff, ← coeff_mul_X_pow]
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ natTrailingDegree p + n ≤ natTrailingDegree (p * X ^ n)
[PROOFSTEP]
rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n : ℕ
⊢ ∀ (y : ℕ), y ∈ support (p * X ^ n) → natTrailingDegree p + n ≤ y
[PROOFSTEP]
intro y hy
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
have key : n ≤ y := by
  rw [mem_support_iff, coeff_mul_X_pow'] at hy
  exact by_contra fun h => hy (if_neg h)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
⊢ n ≤ y
[PROOFSTEP]
rw [mem_support_iff, coeff_mul_X_pow'] at hy
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : (if n ≤ y then coeff p (y - n) else 0) ≠ 0
⊢ n ≤ y
[PROOFSTEP]
exact by_contra fun h => hy (if_neg h)
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ support (p * X ^ n)
key : n ≤ y
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
[GOAL]
case a
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
hp : p ≠ 0
n y : ℕ
hy : coeff p (y - n) ≠ 0
key : n ≤ y
⊢ natTrailingDegree p + n ≤ y
[PROOFSTEP]
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
[PROOFSTEP]
refine' Finset.le_min fun n hn => _
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n ∈ support (p * q)
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
rw [mem_support_iff, coeff_mul] at hn
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
[GOAL]
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ trailingDegree p + trailingDegree q ≤ ↑n
[PROOFSTEP]
refine'
  (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
        (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans
    (le_of_eq _)
[GOAL]
case intro.mk.intro
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd ≠ 0
i j : ℕ
hij : (i, j) ∈ Nat.antidiagonal n
hpq : coeff p (i, j).fst * coeff q (i, j).snd ≠ 0
⊢ ↑(i, j).fst + ↑(i, j).snd = ↑n
[PROOFSTEP]
rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← Nat.mem_antidiagonal]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0
[PROOFSTEP]
rw [hp, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have hq : q ≠ 0 := fun hq =>
  h
    (by rw [hq, mul_zero])
      -- Porting note: Needed to account for different coercion behaviour & add the lemma below
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0
[PROOFSTEP]
rw [hq, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
have : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := fun p ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree p + natTrailingDegree q ≤ natTrailingDegree (p * q)
[PROOFSTEP]
rw [← WithTop.coe_le_coe, WithTop.coe_add, this p, this q, this (p * q), ← trailingDegree_eq_natTrailingDegree hp, ←
  trailingDegree_eq_natTrailingDegree hq, ← trailingDegree_eq_natTrailingDegree h]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree p + trailingDegree q ≤ trailingDegree (p * q)
[PROOFSTEP]
exact le_trailingDegree_mul
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) = trailingCoeff p * trailingCoeff q
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∑ x in Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q), coeff p x.fst * coeff q x.snd =
    trailingCoeff p * trailingCoeff q
[PROOFSTEP]
refine'
  Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) _ fun h => (h (Nat.mem_antidiagonal.mpr rfl)).elim
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ ∀ (b : ℕ × ℕ),
    b ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q) →
      b ≠ (natTrailingDegree p, natTrailingDegree q) → coeff p b.fst * coeff q b.snd = 0
[PROOFSTEP]
rintro ⟨i, j⟩ h₁ h₂
[GOAL]
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j) ∈ Nat.antidiagonal (natTrailingDegree p + natTrailingDegree q)
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [Nat.mem_antidiagonal] at h₁
[GOAL]
case mk
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
by_cases hi : i < p.natTrailingDegree
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
by_cases hj : j < q.natTrailingDegree
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : ¬i < natTrailingDegree p
hj : ¬j < natTrailingDegree q
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
rw [not_lt] at hi hj
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ coeff p (i, j).fst * coeff q (i, j).snd = 0
[PROOFSTEP]
refine' (h₂ (Prod.ext_iff.mpr _).symm).elim
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
i j : ℕ
h₁ : (i, j).fst + (i, j).snd = natTrailingDegree p + natTrailingDegree q
h₂ : (i, j) ≠ (natTrailingDegree p, natTrailingDegree q)
hi : natTrailingDegree p ≤ i
hj : natTrailingDegree q ≤ j
⊢ (natTrailingDegree p, natTrailingDegree q).fst = (i, j).fst ∧
    (natTrailingDegree p, natTrailingDegree q).snd = (i, j).snd
[PROOFSTEP]
exact (add_eq_add_iff_eq_and_eq hi hj).mp h₁.symm
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hp, trailingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hq, trailingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) = trailingDegree p + trailingDegree q
[PROOFSTEP]
refine' le_antisymm _ le_trailingDegree_mul
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ trailingDegree p + trailingDegree q
[PROOFSTEP]
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ← ENat.coe_add]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ trailingDegree (p * q) ≤ ↑(natTrailingDegree p + natTrailingDegree q)
[PROOFSTEP]
apply le_trailingDegree_of_ne_zero
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ coeff (p * q) (natTrailingDegree p + natTrailingDegree q) ≠ 0
[PROOFSTEP]
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hp, trailingCoeff_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have hq : q ≠ 0 := fun hq =>
  h
    (by rw [hq, trailingCoeff_zero, mul_zero])
      -- Porting note: Needed to account for different coercion behaviour & add the lemmas below
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
[PROOFSTEP]
rw [hq, trailingCoeff_zero, mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have aux1 : ∀ n, Nat.cast n = WithTop.some (n) := fun n ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
have aux2 : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) := fun p ↦ rfl
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
[PROOFSTEP]
apply natTrailingDegree_eq_of_trailingDegree_eq_some
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree (p * q) = ↑(natTrailingDegree p + natTrailingDegree q)
[PROOFSTEP]
rw [trailingDegree_mul' h, aux1 (natTrailingDegree p + natTrailingDegree q), WithTop.coe_add, aux2 p, aux2 q, ←
  trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ trailingDegree (-p) = trailingDegree p
[PROOFSTEP]
unfold trailingDegree
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ Finset.min (support (-p)) = Finset.min (support p)
[PROOFSTEP]
rw [support_neg]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Ring R
p : R[X]
⊢ natTrailingDegree (-p) = natTrailingDegree p
[PROOFSTEP]
simp [natTrailingDegree]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Ring R
n : ℤ
⊢ natTrailingDegree ↑n = 0
[PROOFSTEP]
simp only [← C_eq_int_cast, natTrailingDegree_C]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ nextCoeffUp (↑C c) = 0
[PROOFSTEP]
rw [nextCoeffUp]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
c : R
⊢ (if natTrailingDegree (↑C c) = 0 then 0 else coeff (↑C c) (natTrailingDegree (↑C c) + 1)) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natTrailingDegree p
⊢ nextCoeffUp p = coeff p (natTrailingDegree p + 1)
[PROOFSTEP]
rw [nextCoeffUp, if_neg]
[GOAL]
case hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : 0 < natTrailingDegree p
⊢ ¬natTrailingDegree p = 0
[PROOFSTEP]
contrapose! hp
[GOAL]
case hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p : R[X]
hp : natTrailingDegree p = 0
⊢ natTrailingDegree p ≤ 0
[PROOFSTEP]
simpa
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type u_1
n : ℕ∞
h : trailingDegree p < n
h₀ : p = 0
⊢ n ≤ trailingDegree p
[PROOFSTEP]
simp [h₀]


[GOAL]
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all [] p = true ↔ ∀ (a : α), a ∈ [] → p a = true
[PROOFSTEP]
exact iff_of_true rfl (forall_mem_nil _)
[GOAL]
case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
⊢ all (a :: l) p = true ↔ ∀ (a_1 : α), a_1 ∈ a :: l → p a_1 = true
[PROOFSTEP]
simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
a : α
⊢ (all l fun a => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a
[PROOFSTEP]
simp only [all_iff_forall, Bool.of_decide_iff]
[GOAL]
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ any l p = true ↔ ∃ a, a ∈ l ∧ p a = true
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ any [] p = true ↔ ∃ a, a ∈ [] ∧ p a = true
[PROOFSTEP]
exact iff_of_false Bool.not_false' (not_exists_mem_nil _)
[GOAL]
case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : any l p = true ↔ ∃ a, a ∈ l ∧ p a = true
⊢ any (a :: l) p = true ↔ ∃ a_1, a_1 ∈ a :: l ∧ p a_1 = true
[PROOFSTEP]
simp only [any_cons, Bool.or_coe_iff, ih, exists_mem_cons_iff]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
a : α
⊢ (any l fun a => decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a
[PROOFSTEP]
simp [any_iff_exists]


[GOAL]
α : Type u_1
f : Bool → α
⊢ range f = {f false, f true}
[PROOFSTEP]
rw [← image_univ, univ_eq, image_pair]