-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_and_degree_eq_and_monic [Nontrivial S] {p : S[X]} (hlifts : p ∈ lifts f)
    (hp : p.Monic) : ∃ q : R[X], map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
let g : ℕ → R := fun k ↦ (hlifts k).choose

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
let q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
h : q.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f q = p

Tactic:
simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
  map_X, map_C, hg, ← hp.as_sum]

Result:
no goals

Proof state:
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 : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
rw [lifts_iff_coeff_lifts] at hlifts

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
⊢ (∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k).degree < ↑p.natDegree

Tactic:
simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt]

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
h : q.Monic
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Proof state:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic

Tactic:
have hq : map f q = p := by
  simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
    map_X, map_C, hg, ← hp.as_sum]

Result:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k => Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
hq : map f q = p
⊢ ∃ q, map f q = p ∧ q.degree = p.degree ∧ q.Monic