α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) ↔ ∃ a b, b ∈ I ∧ a * y + b = x
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ x ∈ span {y} ⊔ I ↔ ∃ a b, b ∈ I ∧ a * y + b = x
rw [Submodule.mem_sup]
case mp
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) → ∃ a b, b ∈ I ∧ a * y + b = x

case mpr
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ a b, b ∈ I ∧ a * y + b = x) → ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) ↔ ∃ a b, b ∈ I ∧ a * y + b = x
constructor
case mp.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
ya : S
hya : ya ∈ span {y}
b : S
hb : b ∈ I
⊢ ∃ a b_1, b_1 ∈ I ∧ a * y + b_1 = ya + b
case mp
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x) → ∃ a b, b ∈ I ∧ a * y + b = x
rintro ⟨ya, hya, b, hb, rfl⟩
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
b : S
hb : b ∈ I
a : S
hya : a * y ∈ span {y}
⊢ ∃ a_1 b_1, b_1 ∈ I ∧ a_1 * y + b_1 = a * y + b
case mp.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
ya : S
hya : ya ∈ span {y}
b : S
hb : b ∈ I
⊢ ∃ a b_1, b_1 ∈ I ∧ a * y + b_1 = ya + b
obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
no goals
case mp.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
b : S
hb : b ∈ I
a : S
hya : a * y ∈ span {y}
⊢ ∃ a_1 b_1, b_1 ∈ I ∧ a_1 * y + b_1 = a * y + b
exact ⟨a, b, hb, rfl⟩
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
a b : S
hb : b ∈ I
⊢ ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = a * y + b
case mpr
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a b : α
S : Type u_1
inst✝ : CommSemiring S
x y : S
I : Ideal S
⊢ (∃ a b, b ∈ I ∧ a * y + b = x) → ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = x
rintro ⟨a, b, hb, rfl⟩
no goals
case mpr.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : Semiring α
I✝ : Ideal α
a✝ b✝ : α
S : Type u_1
inst✝ : CommSemiring S
y : S
I : Ideal S
a b : S
hb : b ∈ I
⊢ ∃ y_1, y_1 ∈ span {y} ∧ ∃ z, z ∈ I ∧ y_1 + z = a * y + b
exact ⟨a * y, Ideal.mem_span_singleton'.mpr ⟨a, rfl⟩, b, hb, rfl⟩