[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
