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.1181788
rcg : RingHomClass G S R
ι : Sort ?u.1181822
hf : Function.Injective ↑f
x : R
hx : x ∈ comap f ⊥
⊢ x ∈ ⊥
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.1181788
rcg : RingHomClass G S R
ι : Sort ?u.1181822
hf : Function.Injective ↑f
⊢ comap f ⊥ ≤ I
refine' le_trans (fun x hx => _) bot_le
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.1181788
rcg : RingHomClass G S R
ι : Sort ?u.1181822
hf : Function.Injective ↑f
x : R
hx : ↑f x = ↑f 0
⊢ x ∈ ⊥
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.1181788
rcg : RingHomClass G S R
ι : Sort ?u.1181822
hf : Function.Injective ↑f
x : R
hx : x ∈ comap f ⊥
⊢ x ∈ ⊥
rw [mem_comap, Submodule.mem_bot, ← map_zero f] at hx
no goals
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.1181788
rcg : RingHomClass G S R
ι : Sort ?u.1181822
hf : Function.Injective ↑f
x : R
hx : ↑f x = ↑f 0
⊢ x ∈ ⊥
exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥