R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J) ↔ ∀ (z : R), z ∈ I → x * z ∈ J
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ span {x} * I ≤ J ↔ ∀ (z : R), z ∈ I → x * z ∈ J
simp only [mul_le, mem_span_singleton_mul, mem_span_singleton]
case mp
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J) → ∀ (z : R), z ∈ I → x * z ∈ J

case mpr
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (z : R), z ∈ I → x * z ∈ J) → ∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J) ↔ ∀ (z : R), z ∈ I → x * z ∈ J
constructor
case mp
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J
zI : R
hzI : zI ∈ I
⊢ x * zI ∈ J
case mp
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J) → ∀ (z : R), z ∈ I → x * z ∈ J
intro h zI hzI
no goals
case mp
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J
zI : R
hzI : zI ∈ I
⊢ x * zI ∈ J
exact h x (dvd_refl x) zI hzI
case mpr.intro
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (z : R), z ∈ I → x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ x * z * zI ∈ J
case mpr
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
⊢ (∀ (z : R), z ∈ I → x * z ∈ J) → ∀ (r : R), x ∣ r → ∀ (s : R), s ∈ I → r * s ∈ J
rintro h _ ⟨z, rfl⟩ zI hzI
case mpr.intro
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (z : R), z ∈ I → x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ z * (x * zI) ∈ J
case mpr.intro
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (z : R), z ∈ I → x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ x * z * zI ∈ J
rw [mul_comm x z, mul_assoc]
no goals
case mpr.intro
R : Type u
ι : Type ?u.232307
inst✝ : CommSemiring R
I✝ J✝ K L : Ideal R
x : R
I J : Ideal R
h : ∀ (z : R), z ∈ I → x * z ∈ J
z zI : R
hzI : zI ∈ I
⊢ z * (x * zI) ∈ J
exact J.mul_mem_left _ (h zI hzI)