Theorem: Ideal.image_eq_map_of_surjective (unused_files/Ideal.lean)

State before:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ⇑f '' ↑I = ↑(map f I)
Tactic:
symm
State after:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ↑(map f I) = ⇑f '' ↑I

State before:
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
⊢ ↑(map f I) = ⇑f '' ↑I
Tactic:
ext x
State after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ ↑(map f I) ↔ x ∈ ⇑f '' ↑I

State before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ ↑(map f I) ↔ x ∈ ⇑f '' ↑I
Tactic:
simp only [Set.mem_image, SetLike.mem_coe]
State after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ map f I ↔ ∃ x_1 ∈ I, f x_1 = x

State before:
case h
A : Type u_1
B : Type u_2
inst✝¹ : Semiring A
inst✝ : Semiring B
f : A →+* B
I : Ideal A
hf : Function.Surjective ⇑f
x : B
⊢ x ∈ map f I ↔ ∃ x_1 ∈ I, f x_1 = x
Tactic:
apply Ideal.mem_map_iff_of_surjective _ hf
State after:
no goals