case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ rangeS f ↔ x✝ ∈ Subsemiring.map f ⊤
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f✝ f : R →+* S
⊢ rangeS f = Subsemiring.map f ⊤
ext
no goals
case h
R : Type u
S : Type v
T : Type w
inst✝² : NonAssocSemiring R
M : Submonoid R
inst✝¹ : NonAssocSemiring S
inst✝ : NonAssocSemiring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ rangeS f ↔ x✝ ∈ Subsemiring.map f ⊤
simp