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
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
obtain ⟨r, rfl⟩ := Set.mem_range.1 h
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
⊢ ↑(mapRingHom f) (↑C r) = ↑C (↑f r)
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
use C r
no goals
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
⊢ ↑(mapRingHom f) (↑C r) = ↑C (↑f r)
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  and_self_iff]