no goals
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : FG I
f : R →+* S
⊢ FG (Ideal.map f I)
classical
  obtain ⟨s, hs⟩ := h
  refine' ⟨s.image f, _⟩
  rw [Finset.coe_image, ← Ideal.map_span, hs]
case intro
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ FG (Ideal.map f I)
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : FG I
f : R →+* S
⊢ FG (Ideal.map f I)
obtain ⟨s, hs⟩ := h
case intro
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ span ↑(Finset.image (↑f) s) = Ideal.map f I
case intro
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ FG (Ideal.map f I)
refine' ⟨s.image f, _⟩
no goals
case intro
R✝ : Type ?u.327753
M : Type ?u.327756
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ span ↑(Finset.image (↑f) s) = Ideal.map f I
rw [Finset.coe_image, ← Ideal.map_span, hs]