case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ ↑f '' s ⊆ ↑(map f (span s))

case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ map f (span s) ≤ Submodule.span S (↑f '' s)
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ map f (span s) = span (↑f '' s)
refine (Submodule.span_eq_of_le _ ?_ ?_).symm
case refine_1.intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
x : R
hx : x ∈ s
⊢ ↑f x ∈ ↑(map f (span s))
case refine_1
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ ↑f '' s ⊆ ↑(map f (span s))
rintro _ ⟨x, hx, rfl⟩
no goals
case refine_1.intro.intro
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
x : R
hx : x ∈ s
⊢ ↑f x ∈ ↑(map f (span s))
exact mem_map_of_mem f (subset_span hx)
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ ↑f '' s ⊆ ↑(Submodule.span S (↑f '' s))
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ map f (span s) ≤ Submodule.span S (↑f '' s)
rw [map_le_iff_le_comap, span_le, coe_comap, ← Set.image_subset_iff]
no goals
case refine_2
R : Type u
S : Type v
F : Type u_1
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f✝ : F
I J : Ideal R
K L : Ideal S
G : Type ?u.756873
rcg : RingHomClass G S R
f : F
s : Set R
⊢ ↑f '' s ⊆ ↑(Submodule.span S (↑f '' s))
exact subset_span