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