case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ x ∈ ↑(mk I) ⁻¹' (↑(mk I) '' s) ↔ x ∈ ⋃ (x : { x // x ∈ I }), (fun y => ↑x + y) '' s
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
s : Set R
⊢ ↑(mk I) ⁻¹' (↑(mk I) '' s) = ⋃ (x : { x // x ∈ I }), (fun y => ↑x + y) '' s
ext x
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 - x ∈ I) ↔ ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ x ∈ ↑(mk I) ⁻¹' (↑(mk I) '' s) ↔ x ∈ ⋃ (x : { x // x ∈ I }), (fun y => ↑x + y) '' s
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
no goals
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 - x ∈ I) ↔ ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
exact
  ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
    ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
no goals
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ x_1, x_1 ∈ s ∧ x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ ↑{ val := -(a - x), property := (_ : -(a - x) ∈ I) } + a = x
simp
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑{ val := i, property := hi } + a = x
⊢ -↑{ val := i, property := hi } ∈ I
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑{ val := i, property := hi } + a = x
⊢ a - x ∈ I
rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]
no goals
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑{ val := i, property := hi } + a = x
⊢ -↑{ val := i, property := hi } ∈ I
exact I.neg_mem hi