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)

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)
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)
by_cases hzero : s = 0
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)
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)
rw [lifts_iff_set_range] at hl
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)
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)
obtain ⟨q, hq⟩ := hl
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)
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)
replace hq := (ext_iff.1 hq) n
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)
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)
have hcoeff : f (q.coeff n) = s := by
  simp [coeff_monomial] at hq
  exact hq
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
⊢ map f (↑(monomial n) (coeff q n)) = ↑(monomial n) s ∧ degree (↑(monomial n) (coeff q n)) = degree (↑(monomial n) s)
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)
use monomial n (q.coeff n)
case neg.intro.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

case neg.intro.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)
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
⊢ map f (↑(monomial n) (coeff q n)) = ↑(monomial n) s ∧ degree (↑(monomial n) (coeff q n)) = degree (↑(monomial n) s)
constructor
case neg.intro.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)
case neg.intro.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)
have hqzero : q.coeff n ≠ 0 := by
  intro habs
  simp only [habs, RingHom.map_zero] at hcoeff
  exact hzero hcoeff.symm
case neg.intro.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)
case neg.intro.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)
rw [← C_mul_X_pow_eq_monomial]
case neg.intro.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)
case neg.intro.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)
rw [← C_mul_X_pow_eq_monomial]
no goals
case neg.intro.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)
simp only [hzero, hqzero, Ne.def, not_false_iff, degree_C_mul_X_pow]
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
⊢ map f 0 = ↑(monomial n) s ∧ degree 0 = degree (↑(monomial n) s)
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)
use 0
no goals
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
⊢ map f 0 = ↑(monomial n) s ∧ degree 0 = degree (↑(monomial n) s)
simp only [hzero, degree_zero, eq_self_iff_true, and_self_iff, monomial_zero_right,
  Polynomial.map_zero]
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
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
simp [coeff_monomial] at hq
no goals
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
exact hq
no goals
case neg.intro.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
simp only [hcoeff, map_monomial]
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
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
intro habs
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
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
simp only [habs, RingHom.map_zero] at hcoeff
no goals
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
exact hzero hcoeff.symm