English
If monomial n with coefficient s lifts, then there exists a lift q in R[X] such that map f q equals that monomial and q.degree equals that monomial's degree.
Русский
Если мономиал n с коэффициентом s поднимается, существует подъем q в R[X] такой, что map f q = monomial n s и deg(q) = deg(monomial n s).
LaTeX
$$$ \exists q : R[X], \ map\ f\ q = monomial\ n\ s \land q.\deg = (monomial\ n\ s).\deg$$$
Lean4
theorem monomial_mem_lifts_and_degree_eq {s : S} {n : ℕ} (hl : monomial n s ∈ lifts f) :
∃ q : R[X], map f q = monomial n s ∧ q.degree = (monomial n s).degree :=
by
rcases eq_or_ne s 0 with rfl | h
· exact ⟨0, by simp⟩
obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n
refine ⟨monomial n a, map_monomial f, ?_⟩
rw [degree_monomial, degree_monomial n h]
exact mt (fun ha ↦ ha ▸ map_zero f) h
