P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i', i' ∈ I ∧ ∃ j', j' ∈ J ∧ x = i' ⊔ j'
refine' ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, _⟩
no goals
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j
calc
  x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
  _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left