-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_iff_coeffs_subset_range (p : S[X]) :
    p ∈ lifts f ↔ (p.coeffs : Set S) ⊆ Set.range f

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

Tactic:
exact ⟨0, by simp [hn]⟩

Result:
no goals

Proof state:
case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ Set.range ⇑f

Tactic:
obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc

Result:
case mp.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
n : ℕ
hn : a✝ = p.coeff n
⊢ a✝ ∈ Set.range ⇑f

Proof state:
case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) → ↑p.coeffs ⊆ Set.range ⇑f

Tactic:
intro h _ hc

Result:
case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
⊢ a✝ ∈ Set.range ⇑f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : p.coeff n = 0
⊢ f 0 = p.coeff n

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : ¬p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

Tactic:
exact h <| coeff_mem_coeffs _ _ hn

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
⊢ p.coeff n ∈ Set.range ⇑f

Tactic:
by_cases hn : p.coeff n = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : ¬p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ↑p.coeffs ⊆ Set.range ⇑f

Tactic:
rw [lifts_iff_coeff_lifts]

Result:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) ↔ ↑p.coeffs ⊆ Set.range ⇑f

Proof state:
case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ ↑p.coeffs ⊆ Set.range ⇑f → ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Tactic:
intro h n

Result:
case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
⊢ p.coeff n ∈ Set.range ⇑f

Proof state:
case mp.intro.intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
a✝ : S
hc : a✝ ∈ ↑p.coeffs
n : ℕ
hn : a✝ = p.coeff n
⊢ a✝ ∈ Set.range ⇑f

Tactic:
exact hn ▸ h n

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) ↔ ↑p.coeffs ⊆ Set.range ⇑f

Tactic:
constructor

Result:
case mp
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f) → ↑p.coeffs ⊆ Set.range ⇑f

case mpr
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ ↑p.coeffs ⊆ Set.range ⇑f → ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f