case h
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ Subring.map f ⊤
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
⊢ range f = Subring.map f ⊤
ext
no goals
case h
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f✝ f : R →+* S
x✝ : S
⊢ x✝ ∈ range f ↔ x✝ ∈ Subring.map f ⊤
simp