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

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
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
cases' subsingleton_or_nontrivial R with hR hR
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
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
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
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

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
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
by_cases h0 : erase p.natDegree p = 0
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
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
obtain ⟨q, hq⟩ := mem_lifts_and_degree_eq (erase_mem_lifts p.natDegree hlifts)
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
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
have p_neq_0 : p ≠ 0 := by intro hp; apply h0; rw [hp]; simp only [natDegree_zero, erase_zero]
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
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
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
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

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
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
refine' ⟨q + X ^ p.natDegree, _, _, (monic_X_pow _).add_of_right hdeg⟩
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
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
obtain ⟨q, hq⟩ := mem_lifts_and_degree_eq hlifts
no goals
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
exact ⟨q, hq.1, hq.2, monic_of_subsingleton _⟩
no goals
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
simpa only [hp.leadingCoeff, C_1, one_mul, eraseLead] using eraseLead_add_C_mul_X_pow p
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
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
rw [← H, h0, zero_add]
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

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)
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
refine' ⟨X ^ p.natDegree, _, _, monic_X_pow p.natDegree⟩
no goals
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
rw [Polynomial.map_pow, map_X]
no goals
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)
rw [degree_X_pow, degree_X_pow]
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
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
intro hp
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
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
apply h0
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
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
rw [hp]
no goals
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
simp only [natDegree_zero, erase_zero]
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
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)
rw [@degree_X_pow R, hq.2, ←degree_eq_natDegree p_neq_0]
no goals
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
exact degree_erase_lt p_neq_0
no goals
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
rw [Polynomial.map_add, hq.1, Polynomial.map_pow, map_X, H]
no goals
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
rw [degree_add_eq_right_of_degree_lt hdeg, degree_X_pow, degree_eq_natDegree hp.ne_zero]