case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z : R
⊢ span {x + y * z, y} = span {x, y}
ext
case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ x✝ ∈ span {x + y * z, y} ↔ x✝ ∈ span {x, y}
rw [mem_span_pair, mem_span_pair]
no goals
case h
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a b : α
R : Type u
inst✝ : CommRing R
x y z x✝ : R
⊢ (∃ a b, a * (x + y * z) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝
exact
  ⟨fun ⟨a, b, h⟩ =>
    ⟨a, b + a * z, by
      rw [← h]
      ring1⟩,
    fun ⟨a, b, h⟩ =>
    ⟨a, b - a * z, by
      rw [← h]
      ring1⟩⟩
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹
rw [← h]
no goals
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : R
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = a * (x + y * z) + b * y
ring1
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹
rw [← h]
no goals
α : Type u
β : Type v
inst✝¹ : Semiring α
I : Ideal α
a✝ b✝ : α
R : Type u
inst✝ : CommRing R
x y z x✝¹ : R
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : R
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = a * x + b * y
ring1