R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
⊢ ↑f '' ↑I ⊆ ↑(comap g I)
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
⊢ map f I ≤ comap g I
refine' Ideal.span_le.2 _
case intro.intro
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
x : R
hx : x ∈ ↑I
⊢ ↑f x ∈ ↑(comap g I)
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
⊢ ↑f '' ↑I ⊆ ↑(comap g I)
rintro x ⟨x, hx, rfl⟩
case intro.intro
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
x : R
hx : x ∈ ↑I
⊢ x ∈ I
case intro.intro
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
x : R
hx : x ∈ ↑I
⊢ ↑f x ∈ ↑(comap g I)
rw [SetLike.mem_coe, mem_comap, hf hx]
no goals
case intro.intro
R : Type u
S : Type v
F : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
rc : RingHomClass F R S
f : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_1
rcg : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ↑g ↑f ↑I
x : R
hx : x ∈ ↑I
⊢ x ∈ I
exact hx