R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
rw [eq_top_iff_one] at h
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
h : ∃ y, y ∈ I ∧ ∃ z, z ∈ J ∧ y + z = 1
i : R
hi : ∃ y, y ∈ I ∧ ∃ z, z ∈ K ∧ y + z = i
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K
rw [Submodule.mem_sup] at h hi⊢
case intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i : R
hi : ∃ y, y ∈ I ∧ ∃ z, z ∈ K ∧ y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
h : ∃ y, y ∈ I ∧ ∃ z, z ∈ J ∧ y + z = 1
i : R
hi : ∃ y, y ∈ I ∧ ∃ z, z ∈ K ∧ y + z = i
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
obtain ⟨i1, hi1, j, hj, h⟩ := h
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
case intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i : R
hi : ∃ y, y ∈ I ∧ ∃ z, z ∈ K ∧ y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
obtain ⟨i', hi', k, hk, hi⟩ := hi
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ i' + i1 * k + j * k = i
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ ∃ y, y ∈ I ∧ ∃ z, z ∈ J * K ∧ y + z = i
refine' ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, _⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
ι : Type ?u.266258
inst✝ : CommSemiring R
I J K L : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ i' + i1 * k + j * k = i
rw [add_assoc, ← add_mul, h, one_mul, hi]