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

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
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
cases' subsingleton_or_nontrivial S with hR hR
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
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
obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
no goals
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
exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩
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
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
obtain rfl : p = 1 := Subsingleton.elim _ _
no goals
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
refine' ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
no goals
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
simp
no goals
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
simp